Interpolant Strength

Publication Type:

Conference Paper


VMCAI 2010, Springer, Volume 5944, Madrid, p.129-145 (2010)





 Interpolant-based model checking is an approximate method
for computing 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 approx-
imation 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 di erent 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 di erent strength can also be ob-
tained by transforming a resolution proof. We analyse an existing proof
transformation, generalise it, and characterise the interpolants obtained.