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.
['Kenneth L. McMillan']
Applications of craig interpolants in model checking