Sciweavers

Share
TACAS
2005
Springer

Applications of Craig Interpolants in Model Checking

9 years 4 months ago
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.
Kenneth L. McMillan
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where TACAS
Authors Kenneth L. McMillan
Comments (0)
books