Model Checking
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 compatible version. The MathSAT compatible version is able to utilize MathSAT4 as a part of its backend, while the original version does not depend on MathSAT.
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 the 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 file. about 5.1MB
- Model Checking ( MathSAT compatible version ) tgz file. 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
This model checking tool was been developed by the University of Tokyo, with the support of JST CREST "Dependable Embedded Operating System for Practical Uses (DEOS)" project.
