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. © 2012 Springer-Verlag.

Lazy abstraction with interpolants for arrays / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - 7180:(2012), pp. 46-61. (Intervento presentato al convegno 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18 tenutosi a Merida, ven nel 2012) [10.1007/978-3-642-28717-6_7].

Lazy abstraction with interpolants for arrays

Ranise S.;
2012-01-01

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. © 2012 Springer-Verlag.
2012
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-642-28716-9
978-3-642-28717-6
Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.
Lazy abstraction with interpolants for arrays / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - 7180:(2012), pp. 46-61. (Intervento presentato al convegno 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-18 tenutosi a Merida, ven nel 2012) [10.1007/978-3-642-28717-6_7].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333286
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 38
  • ???jsp.display-item.citation.isi??? ND
social impact