mbmc
| Beteiligte Mitarbeiter | Beschreibung | Benchmarks
|
| Lehrstuhl für Rechnerarchitektur | |
| Stefan Kupferschmid, Dipl.-Inf. | Entwickler / Kontakt |
mbmc ist ein Bounded Model Checker für sequentielle Schaltungen. Das Werkzeug wurde für die Suche nach sogenannten Gegenbeispielen für invariante Eigenschaften geschrieben. Der Bounded Model Checker basiert auf dem SAT solver MiraXT. In der Hardware Model Checking Competition 2010 http://fmv.jku.at/hwmcc10 belegte mbmc den sechsten Platz auf erfüllbaren Problemeninstanzen.
Das Eingabe Format ist AIGER. Benchmarks können unter http://fmv.jku.at/hwmcc10/benchmarks.html bezogen werden.