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

lmcs:1152 - Logical Methods in Computer Science, November 1, 2007, Volume 3, Issue 4
Interpolant-Based Transition Relation Approximation

Authors: Jhala, Ranjit and McMillan, Kenneth L.

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.


Source : oai:arXiv.org:0706.0523
DOI : 10.2168/LMCS-3(4:1)2007
Volume: Volume 3, Issue 4
Published on: November 1, 2007
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


Share

Consultation statistics

This page has been seen 91 times.
This article's PDF has been downloaded 25 times.