3 V. D'Silva D. Kroening M. Purandare G. Weissenbacher 2010 Interpolant Strength VMCAI 2010 Madrid Springer 5944 129-145 Lecture Notes in Computer Science 17/01/2010 978-3-642-11318-5 <p><font size="1">&nbsp;Interpolant-based model checking is an approximate method<br />for computing invariants of transition systems. The performance of the<br />model checker is contingent on the approximation computed, which in<br />turn depends on the logical strength of the interpolants. A good approx-<br />imation is coarse enough to enable rapid convergence but strong enough<br />to be contained within the weakest inductive invariant. We present a<br />system for constructing propositional interpolants of di erent strength<br />from a resolution refutation. This system subsumes existing methods and<br />allows interpolation systems to be ordered by the logical strength of the<br />obtained interpolants. Interpolants of di erent strength can also be ob-<br />tained by transforming a resolution proof. We analyse an existing proof<br />transformation, generalise it, and characterise the interpolants obtained.</font></p><p>&nbsp;</p><p>&nbsp;</p><p>&nbsp;</p> http://www.kroening.com/publications/view-publications-dpwk2010.html