Interpolation in theorem proving for program checking

Interpolation is a theorem-proving technique that consists in extracting from a proof of inconsistency an intermediate formula, called interpolant, between the formulae, say A and B, whose conjunction yields the contradiction. The interpolant is made only of symbols shared between A and B and therefore it can be used to capture an intermediate state, if A and B describe program states. It has applications in software model checking and invariant generation. For the latter application it is key to generate interpolants with quantifiers, since invariants often need them. We studied in a systematic way interpolation systems for the proofs produced by key inference engines of state-of-the-art theorem provers: DPLL for propositional logic, DPLL(T) and equality sharing for SMT-solving, superposition-based inference systems for first-order logic with equality, and DPLL(Γ+T). By using a two-stage approach we obtained interpolation systems for general proofs by superposition and by DPLL(Γ+T), including model-based theory combination:


Maria Paola Bonacina