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. © 2014 Springer Science+Business Media New York.

An extension of lazy abstraction with interpolation for programs with arrays / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 45:1(2014), pp. 63-109. [10.1007/s10703-014-0209-9]

An extension of lazy abstraction with interpolation for programs with arrays

Ranise S.;
2014-01-01

Abstract

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. © 2014 Springer Science+Business Media New York.
2014
1
Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.
An extension of lazy abstraction with interpolation for programs with arrays / Alberti, F.; Bruttomesso, R.; Ghilardi, S.; Ranise, S.; Sharygina, N.. - In: FORMAL METHODS IN SYSTEM DESIGN. - ISSN 0925-9856. - 45:1(2014), pp. 63-109. [10.1007/s10703-014-0209-9]
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/332961
 Attenzione

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

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