FOCI

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

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

1 2 3 next

  1. Barrett, Clark; Tinelli, Cesare: Satisfiability modulo theories (2018)
  2. Biere, Armin; Kröning, Daniel: SAT-based model checking (2018)
  3. Cheng, Xi; Zhou, Min; Song, Xiaoyu; Gu, Ming; Sun, Jiaguang: Parallelizing SMT solving: lazy decomposition and conciliation (2018)
  4. McMillan, Kenneth L.: Interpolation and model checking (2018)
  5. Sofronie-Stokkermans, Viorica: On interpolation and symbol elimination in theory extensions (2018)
  6. Christ, Jürgen; Hoenicke, Jochen: Proof tree preserving tree interpolation (2016)
  7. Gan, Ting; Dai, Liyun; Xia, Bican; Zhan, Naijun; Kapur, Deepak; Chen, Mingshuai: Interpolant synthesis for quadratic polynomial inequalities and combination with EUF (2016)
  8. Kroening, Daniel (ed.); Rybalchenko, Andrey (ed.): Preface: Special issue on interpolation (2016)
  9. Monniaux, David: A survey of satisfiability modulo theory (2016)
  10. Schlaipfer, Matthias; Weissenbacher, Georg: Labelled interpolation systems for hyper-resolution, clausal, and local proofs (2016)
  11. Sofronie-Stokkermans, Viorica: On interpolation and symbol elimination in theory extensions (2016)
  12. Totla, Nishant; Wies, Thomas: Complete instantiation-based interpolation (2016)
  13. Bonacina, Maria Paola; Johansson, Moa: Interpolation systems for ground proofs in automated deduction: a survey (2015)
  14. Bonacina, Maria Paola; Johansson, Moa: On interpolation in automated theorem proving (2015)
  15. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation in combinations of equality interpolating theories (2014)
  16. Rasga, João; Sernadas, Cristina; Sernadas, Amlcar: Craig interpolation in the presence of unreliable connectives (2014)
  17. Rollini, Simone Fulvio; Bruttomesso, Roberto; Sharygina, Natasha; Tsitovich, Aliaksei: Resolution proof transformation for compression and interpolation (2014)
  18. Gange, Graeme; Navas, Jorge A.; Stuckey, Peter J.; Søndergaard, Harald; Schachte, Peter: Unbounded model-checking with interpolation for regular language constraints (2013)
  19. Sernadas, C.; Rasga, J.; Sernadas, A.: Preservation of Craig interpolation by the product of matrix logics (2013)
  20. Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio: Quantifier-free interpolation of a theory of arrays (2012)

1 2 3 next