alexander heußner contact teaching tools publications research home


gcv logo

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.

mcscm logo

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! logo

Bench! 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.

PDF icon

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.