Interpolation-Based Verification

Origin. McMillan (2003). Craig interpolants from UNSAT proofs. Approximate forward/backward reachability. Completeness without state explosion. Foundation for modern IC3/PDR.

Models. Interpolant between path segments. Over-approximates reachable states. Refines until fixed point or counterexample. Combines SAT solving with abstraction.

Formalism.

Craig interpolant: Given A ∧ B unsatisfiable: ∃I. A ⊨ I, I ∧ B unsatisfiable, vars(I) ⊆ vars(A) ∩ vars(B).

BMC interpolation: Unroll: I(s₀) ∧ T(s₀,s₁) ∧ ... ∧ T(sₖ₋₁,sₖ) ∧ ¬P(sₖ) Let A = I(s₀), B = rest. Interpolant I₁ over-approximates states reachable in 1 step.

Iterative refinement: I₀ = I(s₀) Iᵢ₊₁ = interpolant for path of length i+1 Continue until Iᵢ₊₁ ⊆ Iᵢ (fixed point) or SAT (counterexample).

Sequence interpolants: A₁ ∧ A₂ ∧ ... ∧ Aₙ unsatisfiable. I₁, I₂, ..., Iₙ₋₁ where: A₁ ⊨ I₁ Iᵢ ∧ Aᵢ₊₁ ⊨ Iᵢ₊₁ Iₙ₋₁ ∧ Aₙ unsatisfiable

Tree interpolants: For recursive programs. Interpolate at procedure boundaries.

IC3/PDR extension: Inductive generalization. Blocking cubes. Property-directed reachability.

Symbols.

Symbol	Unicode	Name	Meaning
I	—	Interpolant	Over-approximation of the states reachable so far
Iᵢ	—	Interpolant sequence	The i-th over-approximation in the iteration
A, B	—	Partition	The two halves of an unsatisfiable conjunction
Aᵢ	—	Sequence conjunct	One factor of A₁ ∧ … ∧ Aₙ in sequence interpolation
⊨	U+22A8	True / Entailment	A ⊨ I, semantic consequence
∧	U+2227	Logical and	Conjunction of the partition or the unrolling
∃	U+2203	There exists	Asserts existence of the interpolant
⊆	U+2286	Subset of or equal to	vars(I) ⊆ vars(A) ∩ vars(B); also the fixed-point test
∩	U+2229	Intersection	Shared vocabulary of the two partitions
¬	U+00AC	Not sign	Negated property at the end of the unrolling
T	—	Transition relation	T(sᵢ, sᵢ₊₁) in the unrolled formula
P	—	Property	Safety predicate being checked
vars	—	Vocabulary	Free variables of a formula

Metatheory. Craig's interpolation theorem (1957) supplies the existence claim for first-order logic, but the method turns on its constructive content: an interpolant can be read off a resolution refutation in time linear in the size of the proof, the propositional case analysed by Krajíček and Pudlák (1997) under the name feasible interpolation. McMillan (2003) used this to convert bounded model checking into a complete procedure. Take A to be the first frame of an unrolling and B the remainder; the interpolant over-approximates the one-step image while remaining expressible in the shared vocabulary, so iterating produces an increasing sequence of over-approximations, and a fixed point Iᵢ₊₁ ⊆ Iᵢ is an inductive invariant establishing the property — unbounded completeness with no diameter computation. Soundness holds because every interpolant contains the exact image; termination is guaranteed on finite-state systems, where the sequence is monotone in a finite lattice. Sequence and tree interpolants extend this to procedure summaries, and IC3/PDR (Bradley 2011) replaces the monolithic unrolling with per-frame inductive generalization.

Applies to. Hardware model checking. Software verification. IC3/PDR. Procedure summaries. Invariant generation.

Limitations. Interpolants are not unique and there is no best one: a refutation determines an interpolant, distinct refutations give incomparable over-approximations, and whether the iteration converges depends on which proof the solver happened to find, so the procedure's behaviour is not a function of the problem alone. Convergence to a fixed point is guaranteed only over finite state; on infinite-state systems the sequence of over-approximations may weaken forever without closing, and Rice's theorem forbids any procedure that always terminates. Interpolation is a property of the theory rather than a given: linear arithmetic and equality with uninterpreted functions admit quantifier-free interpolants, the theory of arrays does not without extending the signature, and theory combinations do not inherit the property automatically. The construction requires the solver to emit a checkable refutation, so any decision procedure that does not produce proofs cannot be used at all.