A model checking tool for analyzing source code written in the C programming language.

Outline

Two versions of the model checking tool are provided: the original version and the MathSAT-ready version. The MathSAT-ready version is able to utilize MathSAT4 as a part of its backend, while the original version does not depend on it.

This tool is provided "AS IS" without warranty or support of any kind.

MathSAT4, which is an SMT solver developed and published by FBK-IRST and University of Trento, is available for research and evaluation purposes in an academic environment only. It cannot be used in a commercial environment, particularly as part of a commercial product, without written permission.

Download

• Model Checking ( original version ) tgz about 5.1MB
• Model Checking ( MathSAT-ready version ) tgz about 5.2MB

Please refer to "README", "INSTALL", and "COPYRIGHT" in the tgz files for further information.

License

The model checking tool itself is licensed under GPL. Further information is available in "COPYRIGHT" and "README" of the tgz files.
The license information for MathSAT4 can be found here.

Acknowledgement

The model checking tool has been developed by the University of Tokyo, with the support of JST CREST "Dependable Embedded Operating System for Practical Uses (DEOS)" project.