CSIsat: Interpolation for LA+EUF

12 years 8 months ago
CSIsat: Interpolation for LA+EUF
We present CSIsat, an interpolating decision procedure for the quantifier-free theory of rational linear arithmetic and equality with uninterpreted function symbols. Our implementation combines the efficiency of linear programming for solving the arithmetic part with the efficiency of a SAT solver to reason about the boolean structure. We evaluate the efficiency of our tool on benchmarks from software verification. Binaries and the source code of CSIsat are publicly available as free software. 1 Overview The Craig interpolant for a pair (1, 2) of formulas such that 1 2 is not satisfiable, is a formula such that 1 implies , the conjunction 2 is not satisfiable, and is over symbols that are common to 1 and 2 [4]. Craig interpolants have been applied successfully in formal verification and logic synthesis. For example, several software verification tools use Craig interpolants derived easible counterexamples to refine their abstractions. An interpolating decision procedure extends a ...
Dirk Beyer, Damien Zufferey, Rupak Majumdar
Added 12 Oct 2010
Updated 12 Oct 2010
Type Conference
Year 2008
Where CAV
Authors Dirk Beyer, Damien Zufferey, Rupak Majumdar
Comments (0)