FOCI: and interpolating prover. FOCI is a decision procedure for quantifier-free first-order formulas. It supports certain interpreted theories, such as equality, uninterpreted functions, linear arithmetic, and arrays. Most importantly, it can compute quantifier-free Craig interpolants for inconsistent pairs (or more generally, sequences) of formulas. This has a number of applications in infinite-state verification, for example, discovering predicates in predicate abstraction, and computing inductive invariants.

References in zbMATH (referenced in 39 articles )

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

1 2 next

  1. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  2. Kroening, Daniel (ed.); Rybalchenko, Andrey (ed.): Preface: Special issue on interpolation (2016)
  3. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  4. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  5. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  6. Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
  7. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation in combinations of equality interpolating theories (2014)
  8. Rasga, João; Sernadas, Cristina; Sernadas, Amlcar: Craig interpolation in the presence of unreliable connectives (2014)
  9. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  10. Gange, Graeme; Navas, Jorge A.; Stuckey, Peter J.; Søndergaard, Harald; Schachte, Peter: Unbounded model-checking with interpolation for regular language constraints (2013)
  11. Sernadas, C.; Rasga, J.; Sernadas, A.: Preservation of Craig interpolation by the product of matrix logics (2013)
  12. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)
  13. Fuchs, Alexander; Goel, Amit; Grundy, Jim; Krstić, Sava; Tinelli, Cesare: Ground interpolation for the theory of equality (2012)
  14. Griggio, Alberto; Le, Thi Thieu Hoa; Sebastiani, Roberto: Efficient interpolant generation in satisfiability modulo linear integer arithmetic (2012)
  15. Gupta, Ashutosh: Improved single pass algorithms for resolution proof reduction (2012)
  16. Kemper, Stephanie: SAT-based verification for timed component connectors (2012)
  17. Lee, Wonchan; Jung, Yungbum; Wang, Bow-Yaw; Yi, Kwangkuen: Predicate generation for learning-based quantifier-free loop invariant inference (2012)
  18. Shved, P.E.; Mutilin, V.S.; Mandrykin, M.U.: Experience of improving the BLAST static verification tool (2012)
  19. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: An interpolating sequent calculus for quantifier-free Presburger arithmetic (2011)
  20. Brillout, Angelo; Kroening, Daniel; Rümmer, Philipp; Wahl, Thomas: Beyond quantifier-free interpolation in extensions of Presburger arithmetic (2011)

1 2 next