mbmc
| project staff | description | benchmarks
|
| Chair of Computer Architecture | |
| Stefan Kupferschmid, Dipl.-Inf. | developer / contact |
mbmc is a Bounded Model Checker for sequential circuits and invariant properties. The tool has been developed in order to detect so-called counterexamples. The underlying SAT-solver is MiraXT. In the Hardware Model Checking Competition 2010 this solver ranked sixth on problem instances that contain a counterexample.
The input format is AIGER. The benchmarks used in the Hardware Model Checking Competition 2010 can be obtained from http://fmv.jku.at/hwmcc10/benchmarks.html.