CIP
Subproject |
H1/2 |
Categories |
Core algorithms |
Overview |
The abbreviation CIP stands for Carig Interpolation Prover. This tool can be used to prove or to disprove invariant properties of sequential circuits. CIP participated in the Hardware Model Checking Competition 2010 and took the third place on instances that contain so-called counterexamples and showed competitive behaviour on benchmarks with a valid invariant property. The solver is a bounded model checker enriched by Craig interpolation in order to find a fixed point in the set of reachable states. Furthermore, CIP contains a preprocessing routine that is useful for incremental solving the different bounded model checking instances and is further compatible with Craig interpolation. |
S. Kupferschmid, M. Lewis, T. Schubert, and B. Becker. Incremental Preprocessing Methods for use in BMC. Formal Methods in System Design, pages 1-20, 2011. |
|
Hardware Model Checking Competition |
|
Download |
Click here for the binary. |
Manual |
Just type ./CIP on the command line to see how it can be used. |
Status |
Stable |