Interpolant Strength
Vijay D'Silva, Daniel Kroening, Mitra Purandare and Georg Weissenbacher abstract
Interpolant-based model checking is a SAT-based, approximate method for computing inductive invariants of transition systems. The performance of the model checker is contingent on the approximation computed, which in turn depends on the logical strength of the interpolants. A good approximation is coarse enough to enable rapid convergence but strong enough to be contained within the weakest inductive invariant. We present a system for constructing propositional interpolants of different strength from a resolution refutation. This system subsumes existing methods and allows interpolation systems to be ordered by the logical strength of the obtained interpolants. Interpolants of different strength can also be obtained by transforming a resolution proof. We analyse an existing proof transformation, generalise it, and characterise the interpolants obtained.
infobook title | Proceedings of the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI) |
month | January |
note | Extended version available as technical report. |
publisher | Springer |
series | Lecture Notes in Computer Science |
volume | 5944 |
year | 2010 |
links
BibTeX
related pages
|
