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

CIP

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |


Beteiligte Mitarbeiter

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


Beschreibung

Die Abkürzen CIP steht für Craig Interpolation Prover. Dieses Werkzeug wird verwendet um invariante Eigenschaften einer sequentiellen Schaltung zu beweisen oder zu widerlegen. CIP hat an der Hardware Model Checking Competition 2010 teilgenommen. Dabei belegte der Model Checker den dritten Platz auf Benchmarks, die ein sogenanntes Gegenbeispiel enthalten. Aber auch auf Benchmarks mit einer gültigen Invariante zeigte CIP gute Performance. CIP erweitert klassisches Bounded Model Checking um Craigsche Interpolation, um sogenannte Fixpunkte zu entdecken. Weiter implementiert CIP eine Preprocessing-Routine des Eingabeproblems, das sowohl kompatibel zum inkrementellen Lösen als auch zur Generierung Craigschen Interpolanten ist.



Benchmarks

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



Publikationen
Stefan Kupferschmid, Matthew Lewis, Tobias Schubert, and Bernd Becker
Incremental preprocessing methods for use in bmc
Formal Methods in System Design, pages 1-20, 2011. 10.1007/s10703-011-0122-4