CIP

| project staff | description | benchmarks | publications |

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.

The input format is AIGER. The benchmarks used in the Hardware Model Checking Competition 2010 can be obtained from http://fmv.jku.at/hwmcc10/benchmarks.html