Lazy Abstraction with Interpolants for Arrays

Abstract:

Lazy abstraction with interpolants has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method shows an intrinsic limitation, due to the fact that successful invariants usually contain universally quantified variables, which are not present in the program specification. In this work we present an extension of the interpolation-based lazy abstraction in which arrays of unknown length can be handled in a natural manner. In particular, we exploit the Model Checking Modulo Theories framework to derive a backward reachability version of lazy abstraction that embeds array reasoning. The approach is generic, in that it is valid for both parameterized systems and imperative programs. We show by means of experiments that our approach can synthesize an prove universally quantified properties over arrays in a completely automatic fashion.

Notes:

• BibTex

@inproceedings { ABGRS_LPAR12,
	title = {Lazy Abstraction with Interpolants for Arrays},
	booktitle = {18th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR)},
	year = {2012},
	note = {Extended version. The original publication is available at www.springerlink.com.},
	publisher = {Springer},
	organization = {Springer},
	address = {Mérida, Venezuela},
	author = {Francesco Alberti and  Roberto Bruttomesso and  Silvio Ghilardi and  Silvio Ranise and  Natasha Sharygina}
}