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.
Keywords for this software
References in zbMATH (referenced in 9 articles )
Showing results 1 to 9 of 9.
- Kroening, Daniel (ed.); Rybalchenko, Andrey (ed.): Preface: Special issue on interpolation (2016)
- Leroux, Jér^ome; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
- Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
- Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
- Lee, Wonchan; Jung, Yungbum; Wang, Bow-Yaw; Yi, Kwangkuen: Predicate generation for learning-based quantifier-free loop invariant inference (2012)
- Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)
- Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
- Kroening, Daniel; Leroux, Jér^ome; Rümmer, Philipp: Interpolating quantifier-free Presburger arithmetic (2010)
- Rybalchenko, Andrey; Sofronie-Stokkermans, Viorica: Constraint solving for interpolation (2010)