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 52 articles )

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

1 2 3 next

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

1 2 3 next