Uni-Logo
English       Login
Rechnerarchitektur
        Startseite         |         Institut für Informatik         |         Technische Fakultät
 

mbmc

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks |


Beteiligte Mitarbeiter

Lehrstuhl für Rechnerarchitektur
Stefan Kupferschmid, Dipl.-Inf. Entwickler / Kontakt


Beschreibung

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.



Benchmarks

Das Eingabe Format ist AIGER. Benchmarks können unter http://fmv.jku.at/hwmcc10/benchmarks.html bezogen werden.