CIP

| Beteiligte Mitarbeiter | Beschreibung | Benchmarks | Publikationen |

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.

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