Interpolation Guided Compositional Verification

Model checking suffers from the state space explosion problem. Compositional verification techniques such as assume-guarantee reasoning (AGR) have been proposed to alleviate the problem. However, there are at least three challenges in applying AGR. Firstly, given a system M-1 parallel to M-2, how do we automatically construct and refine (in the presence of spurious counterexamples) an assumption A(2), which must be an abstraction of M-2? Previous approaches suggest to incrementally learn and modify the assumption through multiple invocations of a model checker, which could be often time consuming. Secondly, how do we keep the state space small when checking M-1 parallel to A(2) satisfies phi if multiple refinements of A(2) are necessary? Lastly, in the presence of multiple parallel components, how do we partition the components? In this work, we propose interpolation-guided compositional verification. The idea is to tackle three challenges by using interpolations to generate and refine the abstraction of M-2, to abstract M-1 at the same time (so that the state space is reduced even if A(2) is refined all the way to M-2), and to find good partitions. Experimental results show that the proposed approach outperforms existing approaches consistently.