Lazy abstraction with interpolants for arrays

Francesco Alberti, Roberto Bruttomesso, Silvio Ghilardi, Silvio Ranise, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 and prove universally quantified properties over arrays in a completely automatic fashion.

Original languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages46-61
Number of pages16
Volume7180 LNCS
DOIs
Publication statusPublished - 2012
Event18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18 - Merida, Venezuela, Bolivarian Republic of
Duration: Mar 11 2012Mar 15 2012

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7180 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18
CountryVenezuela, Bolivarian Republic of
CityMerida
Period3/11/123/15/12

    Fingerprint

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., & Sharygina, N. (2012). Lazy abstraction with interpolants for arrays. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7180 LNCS, pp. 46-61). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7180 LNCS). https://doi.org/10.1007/978-3-642-28717-6_7