Home

MuChecker is a model checker for checking properties of context free proccesses expressed in mu calculus. The implementation is the algorithm presented in 1997 by Olof Burkart and Bernhard Steffen in their paper Model checking the full modal mu-calculus for infinite sequential processes.

The model checker currently has a command line interface, as well as an Android gui.

[Building instructions]
[User guides]