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.

References in zbMATH (referenced in 15 articles )

Showing results 1 to 15 of 15.
Sorted by year (citations)

  1. Gan, Ting; Dai, Liyun; Xia, Bican; Zhan, Naijun; Kapur, Deepak; Chen, Mingshuai: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF (2016)
  2. Kroening, Daniel (ed.); Rybalchenko, Andrey (ed.): Preface: Special issue on interpolation (2016)
  3. Leroux, Jér^ome; Rümmer, Philipp; Subotić, Pavle: Guiding Craig interpolation with domain-specific abstractions (2016)
  4. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  5. Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
  6. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation in combinations of equality interpolating theories (2014)
  7. Lee, Wonchan; Jung, Yungbum; Wang, Bow-Yaw; Yi, Kwangkuen: Predicate generation for learning-based quantifier-free loop invariant inference (2012)
  8. Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)
  9. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
  10. Jung, Yungbum; Lee, Wonchan; Wang, Bow-Yaw; Yi, Kwangkuen: Predicate generation for learning-based quantifier-free loop invariant inference (2011)
  11. Kroening, Daniel; Leroux, Jér^ome; Rümmer, Philipp: Interpolating quantifier-free Presburger arithmetic (2010)
  12. Rybalchenko, Andrey; Sofronie-Stokkermans, Viorica: Constraint solving for interpolation (2010)
  13. Cimatti, Alessandro; Griggio, Alberto; Sebastiani, Roberto: Interpolant generation for UTVPI (2009)
  14. Goel, Amit; Krstić, Sava; Tinelli, Cesare: Ground interpolation for combined theories (2009)
  15. Beyer, Dirk; Zufferey, Damien; Majumdar, Rupak: CSIsat: Interpolation for LA+EUF. Tool paper (2008) ioport