Interpolant-Based Transition Relation Approximation

In predicate abstraction, exact image computation is problematic, requiringin the worst case an exponential number of calls to a decision procedure. Forthis reason, software model checkers typically use a weak approximation of theimage. This can result in a failure to prove a property, even given an adequateset of predicates. We present an interpolant-based method for strengthening theabstract transition relation in case of such failures. This approach guaranteesconvergence given an adequate set of predicates, without requiring an exactimage computation. We show empirically that the method converges more rapidlythan an earlier method based on counterexample analysis.Comment: Conference Version at CAV 2005. 17 Pages, 9 Figure