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
A, B	—	Partition	Formula split
⊨	U+22A8	Entails	Implication
vars	—	Variables	Symbol set

Metatheory. Sound and complete for finite systems. Termination via fixed point. Interpolant quality matters. Proof-based construction.

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

Limitations. Interpolant choice affects performance. Sequence interpolation variants. Proof production overhead. Not always best abstraction.