The Grand Central Verifier (GCV) is a tool for verifying asynchronous programs written with Grand Central Dispatch/libdispatch. GCV is currently being implemented and will be published soon.

Detailed information about the Model Checker for Systems of Communicating fifo Machines can be found here.

In a nutshell: this tool implements CEGAR based safety verification with the help of path-invariant based abstration refinement for communicating fifo systems.

Bench!

...is a simple benchmarking framework that frontends the recurring task of relaunching a series of benchmarks with a set of Python scripts and a prototypical cgi-interface. A more detailed presentation can be found here.

trace2dot.py

Small script that takes the output of SMV/ NuSMV and transfers it to the dot-format. Usefull if you just want to see a (counterexample) trace generated by these model checkers without using some of the existing GUIs.