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

    11 Documents citing this article

    Share

    Consultation statistics

    This page has been seen 350 times.
    This article's PDF has been downloaded 249 times.