Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

149

Voted

TACAS
2005
Springer

113views Algorithms» more TACAS 2005»

Applications of Craig Interpolants in Model Checking

15 years 10 months ago

Applications of Craig Interpolants in Model Checking

Download www.kenmcmil.com

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 eﬃciently derived from a refutation of A ∧ B, for certain theories and proof systems. We will discuss a number of applications of this concept in ﬁnite- and inﬁnite-state model checking.

Kenneth L. McMillan

Real-time Traffic

Algorithms | Common Variables | Craig Interpolant | Inconsistent Pair | TACAS 2005 |

claim paper

Related Content

» Efficient Craig Interpolation for Linear Diophantine DisEquations and Linear Modular Equat...

» Stepping forward with interpolants in unbounded model checking

» An Interpolating Theorem Prover

» Interpolation and SATBased Model Checking

» Interpolant Generation for UTVPI

» Leveraging Interpolant Strength in Model Checking

» Improvements to the Implementation of InterpolantBased Model Checking

» Interpolant Learning and Reuse in SATBased Model Checking

» Computing Optimized Representations for Nonconvex Polyhedra by Detection and Removal of Re...

Post Info
More Details (n/a)

Added	28 Jun 2010
Updated	28 Jun 2010
Type	Conference
Year	2005
Where	TACAS
Authors	Kenneth L. McMillan

Comments (0)