An extension of lazy abstraction with interpolation for programs with arrays

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

Research output: Contribution to journalArticle

17 Citations (Scopus)

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 languageEnglish
Pages (from-to)63-109
Number of pages47
JournalFormal Methods in System Design
Volume45
Issue number1
DOIs
Publication statusPublished - 2014

Fingerprint

Interpolation
Interpolate
Model checking
Specifications
Reachability
Model Checking
Modulo
Refinement
Reasoning
Experiments
Benchmark
Specification
Unknown
Invariant
Abstraction
Range of data
Experiment
Framework

Keywords

  • Array programs
  • Lazy abstraction
  • Model checking
  • SMT

ASJC Scopus subject areas

  • Software
  • Hardware and Architecture
  • Theoretical Computer Science

Cite this

Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., & Sharygina, N. (2014). An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods in System Design, 45(1), 63-109. https://doi.org/10.1007/s10703-014-0209-9

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 journalArticle

Alberti, F, Bruttomesso, R, Ghilardi, S, Ranise, S & Sharygina, N 2014, 'An extension of lazy abstraction with interpolation for programs with arrays', Formal Methods in System Design, vol. 45, no. 1, pp. 63-109. https://doi.org/10.1007/s10703-014-0209-9
Alberti, Francesco ; Bruttomesso, Roberto ; Ghilardi, Silvio ; Ranise, Silvio ; Sharygina, Natasha. / An extension of lazy abstraction with interpolation for programs with arrays. In: Formal Methods in System Design. 2014 ; Vol. 45, No. 1. pp. 63-109.
@article{c767e5e419d141deae21ac19e06d40a6,
title = "An extension of lazy abstraction with interpolation for programs with arrays",
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.",
keywords = "Array programs, Lazy abstraction, Model checking, SMT",
author = "Francesco Alberti and Roberto Bruttomesso and Silvio Ghilardi and Silvio Ranise and Natasha Sharygina",
year = "2014",
doi = "10.1007/s10703-014-0209-9",
language = "English",
volume = "45",
pages = "63--109",
journal = "Formal Methods in System Design",
issn = "0925-9856",
publisher = "Springer Netherlands",
number = "1",

}

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 -