This is the source code and binaries distribution of the Faulty Model Checker, the model checker can be executed by running:

faulty-check

you need to set the evironment variable 'FAULTY' with:

export FAULTY = <path to jar files

The first parameter of faulty-check is the program in the Faulty programming language and the second parameter is a file containing the properties to be checked. Some example can be found in the folder: tests/

You can compile the tool by using ant, the source code is available at src/.

This is the first version of the tool, we expect to add further features and examples soon.

*CHANGES of Version 1.1

• Parameters were added to the processes.
• Enum types supported.
• Some improvements in the performance.