Abstraction and Acceleration in SMT-based Model-Checking for Array Programs

Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence phenomena in a satisfactory way. Acceleration is an approach which is widely used to avoid divergence, but it has been applied mostly to integer programs. This paper addresses the problem of accelerating transition relations for unbounded arrays with the ultimate goal of avoiding divergence during reachability analysis of ab-stract programs. For this, we first design a format to compute accelerations in this domain; then we show how to adapt the so-called ‘monotonic abstraction ’ technique to efficiently handle complex formulæ with nested quantifiers generated by the accel-eration preprocessing. Notably, our technique can be easily plugged-in into abstrac-tion/refinement loops, and strongly contributes to avoid divergence: experiments con-ducted with the MCMT model checker attest the effectiveness of our approach on pro-grams with unbounded arrays, where acceleration and abstraction/refinement tech-nologies fail if applied alone