Technical report detail

Tackling divergence: abstraction and acceleration in array programs

by Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

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 abstract 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 formulae with nested quantifiers generated by the acceleration preprocessing. Notably, our technique can be easily plugged-in into abstraction/refinement loops, and strongly contributes to avoid divergence: experiments conducted with the MCMT model checker attest the effectiveness of our approach on programs with unbounded arrays, where acceleration and abstraction/refinement technologies fail if applied alone.

Technical report 2012/01, October 2012

BibTex entry

@techreport{12tackling, author = {Francesco Alberti and Silvio Ghilardi and Natasha Sharygina}, title = {Tackling divergence: abstraction and acceleration in array programs}, institution = {University of Lugano}, number = {2012/01}, year = 2012, month = oct }