Interpolation and SAT-Based Model Checking

By Kenneth L. McMillan. International Conference on Computer Aided Verification, 2003

1,038 citations recorded by the source corpus.

Subfields: Computational Theory and Mathematics, Software

View Paper: https://www.semanticscholar.org/paper/e82fe405bcc7dddd9d3feb04444b405422c69dd1

How researchers see this paper

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

In Computational Theory and Mathematics

In Software

Citations in the corpus

History of Interactive Theorem Proving (2014, background): “As with first-order provers, many SAT solvers are capable of emitting proofs (usually recast as resolution proofs even if that doesn’t reflect how they were found), which have applications not only in proof-checking but for invariant generation via interpolation [McMillan, 2003].”
An interpolating theorem prover (2005, methodology): “In [7] a method of approximate image computation is described that is based on interpolation, and does not require quantifier elimination.”
The nuXmv Symbolic Model Checker (2014, methodology): “Similarly to the finite case, we provide an SMT based implementation for the McMillan approach [5], the interpolation sequence approach [6], k-induction [7] and for algorithms based on IC3 [20,21].”
Model checking (2009, neutral): “37 But, the problem remains a topic of active research.”
SAT-Based Model Checking without Unrolling (2011, methodology): “The stepwise over-approximation structure of F 0 , F 1 , F 2 , . . . , F k is similar to that of interpolation-based model checking (ITP), which uses an interpolant from an unsatisﬁable K -step BMC query to compute the post-image approximately [21].”
PicoSAT Essentials (2008, background): “In approximative image computation, or more general in over approximation of quantiﬁer elimination, a resolution proof obtained from a proof trace allows to generate interpolants [26].”
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].”
Lazy Abstraction with Interpolants (2006, methodology): “The method is also closely related to the interpolation-based model checking method of [10].”
Model Checking and the State Explosion Problem (2011, methodology): “Other techniques for making BMC complete are cube enlargement [18], circuit co-factoring [14], and Craig interpolants [19].”
Abstractions from proofs (2004, methodology): “Inspired by the use of Craig Interpolation for image-computation in [22], we introduce a method by which the proof can be sliced to yield the relevant facts at each point of the trace.”
Efficient implementation of property directed reachability (2011, methodology): “The experimental analysis of Section 6 shows that PDR represents a major performance improvement over interpolation based model checking (IMC) [7], hitherto regarded as the strongest bit-level engine.”