Interpolant Strength

Conference item

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.

Authors: D'Silva, V; Kroening, D; Purandare, M; Weissenbacher, G

• Publisher: Springer
• Host title: Proceedings of the International Conference on Verification‚ Model Checking‚ and Abstract Interpretation (VMCAI)
• Volume: 5944
• Publication date: 2010-01-01
• DOI: 10.1007/978-3-642-11319-2_12