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 ...

• Type: Conference
• Year: 2008
• Where: CAV
• Authors: Dirk Beyer, Damien Zufferey, Rupak Majumdar
• Keywords: CAV 2008, Craig Interpolant, Hardware, Interpolating Decision Procedures, Uninterpreted Function Symbols