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.

Some papers on FOCI

BibTeXPDFKenneth L. McMillan: An interpolating theorem prover. Theor. Comput. Sci. 345(1): 101-121 (2005)
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: A Practical and Complete Approach to Predicate Refinement. TACAS 2006: 459-473
BibTeXPDFRanjit Jhala, Kenneth L. McMillan: Interpolant-Based Transition Relation Approximation. CAV 2005: 39-51
BibTeXPDFKenneth L. McMillan: Applications of Craig Interpolants in Model Checking. TACAS 2005: 1-12
BibTeXPDFThomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, Kenneth L. McMillan: Abstractions from proofs. POPL 2004: 232-244

Download FOCI

FOCI is available in binary form, both as a stand-alone application and as a library. Bindings are available for ocaml and C++. The license allows you to use it for research purposes, but not for commercial applications. Please read the license agreement carefully before downloading.

Read the license agreement and download FOCI from Cadence Berkeley Labs

Last modified: Fri May 26 18:38:54 PDT 2006