Accelerating Interpolation-Based Model-Checking

Interpolation-based model-checking and acceleration techniques have been widely proved successful and efficient for reachability checking. Surpris- ingly, 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 refin- ing 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 spuri- ous 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. Abstract Refine