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.

Publications

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.

Benchmarks

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