An interpolating theorem prover

By Kenneth L. McMillan. Theoretical Computer Science, 2005

306 citations recorded by the source corpus.

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Lazy Abstraction with Interpolants (2006, methodology): “If Γ is quantifier-free, we can derive a quantifier-free interpolant for Γ from a refutation of Γ , in certain interpreted theories [11].”
The software model checker Blast (2007, methodology): “The decision procedures underlying BLAST, which are used for computing reachable regions and interpolants of path formulas, implement linear arithmetic and uninterpreted functions [31, 64, 71].”
Software model checking (2009, unknown): “An interpolant always exists in case ( φ − , φ + ) are ﬁrst-order formulas [Craig 1957], and an interpolant can be constructed in time linear in the size of a resolution proof for formulas in the combination theories of equality with uninterpreted functions and linear arithmetic [McMillan 2004].”
Handbook of Satisfiability (2021, methodology): “The use of interpolation in formal verification was introduced by McMillan in [101] for purely-propositional formulas, and it was subsequently extended to handle TE ∪ TR-formulas in [102].”