Applications of Craig Interpolants in Model Checking

Abstract. A Craig interpolant for a mutually inconsistent pair of formulas (A, B) is a formula that is (1) implied by A, (2) inconsistent with B, and (3) expressed over the common variables of A and B. An interpolant can be efficiently derived from a refutation of A ∧ B, for certain theories and proof systems. We will discuss a number of applications of this concept in finite- and infinite-state model checking.

• Type: Conference
• Year: 2005
• Where: TACAS
• Authors: Kenneth L. McMillan
• Keywords: Algorithms, Common Variables, Craig Interpolant, Inconsistent Pair, TACAS 2005