Ranjit Jhala ; Kenneth L. McMillan - Interpolant-Based Transition Relation Approximation

lmcs:1152 - Logical Methods in Computer Science, November 1, 2007, Volume 3, Issue 4 - https://doi.org/10.2168/LMCS-3(4:1)2007
Interpolant-Based Transition Relation Approximation

Authors: Ranjit Jhala ; Kenneth L. McMillan

In predicate abstraction, exact image computation is problematic, requiring in the worst case an exponential number of calls to a decision procedure. For this reason, software model checkers typically use a weak approximation of the image. This can result in a failure to prove a property, even given an adequate set of predicates. We present an interpolant-based method for strengthening the abstract transition relation in case of such failures. This approach guarantees convergence given an adequate set of predicates, without requiring an exact image computation. We show empirically that the method converges more rapidly than an earlier method based on counterexample analysis.

Volume: Volume 3, Issue 4
Published on: November 1, 2007
Accepted on: June 25, 2015
Submitted on: June 12, 2006
Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Computer Science - Software Engineering,D.2.4,F.3.1


Consultation statistics

This page has been seen 313 times.
This article's PDF has been downloaded 230 times.