[null, {"document_url": "https://link.springer.com/article/10.1007%2Fs10703-014-0209-9", "unformatted_src": "https://media.springernature.com/w306/springer-static/cover/journal/10703/45/1.jpg", "src": "https://media.springernature.com/w306/springer-static/cover/journal/10703/45/1.jpg"}, null]


Formal Methods in System Design 
August 2014, Volume 45, Issue 1, pp 63–109 | Cite as

An extension of lazy abstraction with interpolation for programs with arrays



Lazy abstraction with interpolation-based refinement has been shown to be a powerful technique for verifying imperative programs. In presence of arrays, however, the method suffers from an intrinsic limitation, due to the fact that invariants needed for verification usually contain universally quantified variables, which are not present in program specifications. In this work we present an extension of the interpolation-based lazy abstraction framework 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 supports reasoning about arrays. The new approach has been implemented in a tool, called safari, which has been validated on a wide range of benchmarks. We show by means of experiments that our approach can synthesize and prove universally quantified properties over arrays in a completely automatic fashion.


SMT Model checking Lazy abstraction Array programs

This paper combines and extends materials previously published in [4, 5].



The authors would like to thank the anonymous reviewers for their comments and criticisms that helped to improve the quality of the paper. The work of the first author was supported by the Hasler Foundation under project 09047 and that of the fourth author was partially supported by the “SIAM” project founded by Provincia Autonoma di Trento in the context of the “team 2009—Incoming” COFUND action of the European Commission (FP7). The third author would like to acknowledge the support of the PRIN 2010-2011 project “Logical Methods for Information Management” funded by the Italian Ministry of Education, University and Research (MIUR).



© Springer Science+Business Media New York 2014




Alberti, F., Bruttomesso, R., Ghilardi, S. et al. Form Methods Syst Des (2014) 45: 63. https://doi.org/10.1007/s10703-014-0209-9



