Model Checking @CMU









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

Check out the benchmarks examples done with BMC.











CMU-SCS Model Checking home page

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