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.
Details
| Book Title |
Proceedings of the International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI) |
| Month |
January |
| Note |
Extended version available as technical report. Download slides. |
| Pages |
129−145 |
| Publisher |
Springer |
| Series |
Lecture Notes in Computer Science |
| Volume |
5944 |
| Year |
2010 |
Links
DOI (10.1007/978-3-642-11319-2_12)
Related pages
|
People |