Sciweavers

TACAS
2004
Springer

An Interpolating Theorem Prover

14 years 5 months ago
An Interpolating Theorem Prover
We present a method of deriving Craig interpolants from proofs in the quantifier-free theory of linear inequality and uninterpreted function symbols, and an interpolating theorem prover based on this method. The prover has been used for predicate refinement in the Blast software model checker, and can also be used directly for model checking infinite-state systems, using interpolation-based image approximation. Key words: Craig interpolation, Model Checking, Decision procedures, Infinite-state systems PACS:
Kenneth L. McMillan
Added 02 Jul 2010
Updated 02 Jul 2010
Type Conference
Year 2004
Where TACAS
Authors Kenneth L. McMillan
Comments (0)