Bounded Model Checker: BMC

This is the first release of `BMC' (bounded model checker). It is still considered alpha software and should be handled with great care. A lot of features are missing. Please keep in mind that this tool was purely made for reasearch purposes.

Armin Biere, February 1999

• bmc-1-0-f.tar.gz (more bug fixes, July 14, 1999)
• bmc-1-0-e.tar.gz (fixed bug in inner substitution, June 30, 1999)
• bmc-1-0-c.tar.gz (bug fixes + better counterexample generation (scamid), June 21, 1999)
• bmc-1.0b.tar.gz

CMU-SCS Model Checking home page

Please send any comments and suggestions to  Nishant Sinha - (nishants) at cs dot cmu dot edu.