Interpolation-based model-checking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surprisingly, these two techniques have never been combined to strengthen each other. Intuitively, acceleration provides under-approximation of the reachability set by computing the exact effect of some control-flow cycles and combining them with other transitions. On the other hand, interpolation-based model-checking is refining an over-approximation of the reachable states based on spurious error-traces. The goal of this paper is to combine acceleration techniques with interpolation-based model-checking at the refinement stage. Our method, called "interpolant acceleration", helps to refine the abstraction, ruling out not only a single spurious error-trace but a possibly infinite set of error-traces obtained by any unrolling of its cycles. Interpolant acceleration is also proved to strictly enlarge the set of transformations that can be usually handled by acceleration techniques. © 2008 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Caniart, N., Fleury, E., Leroux, J., & Zeitoun, M. (2008). Accelerating interpolation-based model-checking. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4963 LNCS, pp. 428–442). https://doi.org/10.1007/978-3-540-78800-3_32
Mendeley helps you to discover research relevant for your work.