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.
| Original language | English |
|---|---|
| Pages (from-to) | 63-109 |
| Number of pages | 47 |
| Journal | Formal Methods in System Design |
| Volume | 45 |
| Issue number | 1 |
| DOIs | |
| Publication status | Published - 2014 |
Fingerprint
Keywords
- Array programs
- Lazy abstraction
- Model checking
- SMT
ASJC Scopus subject areas
- Software
- Hardware and Architecture
- Theoretical Computer Science
Cite this
An extension of lazy abstraction with interpolation for programs with arrays. / Alberti, Francesco; Bruttomesso, Roberto; Ghilardi, Silvio; Ranise, Silvio; Sharygina, Natasha.
In: Formal Methods in System Design, Vol. 45, No. 1, 2014, p. 63-109.Research output: Contribution to journal › Article
}
TY - JOUR
T1 - An extension of lazy abstraction with interpolation for programs with arrays
AU - Alberti, Francesco
AU - Bruttomesso, Roberto
AU - Ghilardi, Silvio
AU - Ranise, Silvio
AU - Sharygina, Natasha
PY - 2014
Y1 - 2014
N2 - 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.
AB - 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.
KW - Array programs
KW - Lazy abstraction
KW - Model checking
KW - SMT
UR - http://www.scopus.com/inward/record.url?scp=84905919725&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84905919725&partnerID=8YFLogxK
U2 - 10.1007/s10703-014-0209-9
DO - 10.1007/s10703-014-0209-9
M3 - Article
AN - SCOPUS:84905919725
VL - 45
SP - 63
EP - 109
JO - Formal Methods in System Design
JF - Formal Methods in System Design
SN - 0925-9856
IS - 1
ER -