We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {phi} prog {psi} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.

De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2015). A rule-based verification strategy for array manipulating programs. FUNDAMENTA INFORMATICAE, 140(3-4), 329-355 [10.3233/FI-2015-1257].

A rule-based verification strategy for array manipulating programs

PETTOROSSI, ALBERTO;
2015

Abstract

We present a method for verifying properties of imperative programs that manipulate integer arrays. Imperative programs and their properties are represented by using Constraint Logic Programs (CLP) over integer arrays. Our method is refutational. Given a Hoare triple {phi} prog {psi} that defines a partial correctness property of an imperative program prog, we encode the negation of the property as a predicate incorrect defined by a CLP program P, and we show that the property holds by proving that incorrect is not a consequence of P. Program verification is performed by applying a sequence of semantics preserving transformation rules and deriving a new CLP program T such that incorrect is a consequence of P iff it is a consequence of T. The rules are applied according to an automatic strategy whose objective is to derive a program T that satisfies one of the following properties: either (i) T is the empty set of clauses, hence proving that incorrect does not hold and prog is correct, or (ii) T contains the fact incorrect, hence proving that prog is incorrect. Our transformation strategy makes use of an axiomatization of the theory of arrays for the manipulation of array constraints, and also applies the widening and convex hull operators for the generalization of linear integer constraints. The strategy has been implemented in the VeriMAP transformation system and it has been shown to be quite effective and efficient on a set of benchmark array programs taken from the literature.
Pubblicato
Rilevanza internazionale
Articolo
Esperti anonimi
Settore ING-INF/05 - Sistemi di Elaborazione delle Informazioni
eng
De Angelis, E., Fioravanti, F., Pettorossi, A., & Proietti, M. (2015). A rule-based verification strategy for array manipulating programs. FUNDAMENTA INFORMATICAE, 140(3-4), 329-355 [10.3233/FI-2015-1257].
De Angelis, E; Fioravanti, F ; Pettorossi, A; Proietti, M
Articolo su rivista
File in questo prodotto:
File Dimensione Formato  
DFPP_CILC-13_FundInf@IOS.pdf

non disponibili

Descrizione: Articolo principale
Licenza: Non specificato
Dimensione 215.84 kB
Formato Adobe PDF
215.84 kB Adobe PDF   Visualizza/Apri   Richiedi una copia

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: http://hdl.handle.net/2108/152647
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 9
  • ???jsp.display-item.citation.isi??? 8
social impact