Adaptive interpolation-based model checking

Interpolation-based model checking (IMC) is an important technique in modern formal verification tools. In essence, it relies on an abstraction and refinement process to derive an adequate image approximation for the reachability analysis. However, previous IMC algorithms only offer fixed degrees of abstraction and thus may fail in the proofs if the abstraction is too coarse- or fine-grained. In this paper, we propose an adaptive interpolation-based model checking algorithm in which the degree of abstraction can be adjusted on demand. That is, during the proof process, we closely monitor the effectiveness of the interpolation-based over-approximated image computation and thus adjust the degree of abstraction for the best performance. The experimental results confirm that our flexible interpolation indeed leads to an adequate degree of abstraction as our IMC algorithm outperforms previous ones in various aspects.