M.: Accelerating Interpolation-Based ModelChecking

Abstract. 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 o