In previous work we presented a model checking procedure for linear programs, i.e. programs in which variables range over a numeric domain and expressions involve linear combinations of the variables. In this paper we lift our model checking procedure for linear programs to deal with arrays via iterative abstraction refinement. While most approaches are based on predicate abstraction and therefore the abstraction is relative to sets of predicates, in our approach the abstraction is relative to sets of variables and array indexes, and the abstract program can express complex correlations between program variables and array elements. Thus, while arrays are problematic for most of the approaches based on predicate abstraction, our approach treats them in a precise way.This is an important feature as arrays are ubiquitous in programming. We provide a detailed account of both the abstraction and the refinement processes, discuss their implementation in the eureka tool, and present experimental results that confirm the effectiveness of our approach on a number of programs of interest.

Abstraction Refinement of Linear Programs with Arrays / Armando, A; Benerecetti, Massimo; Mantovani, J.. - STAMPA. - LNCS 4424:(2007), pp. 373-388. (Intervento presentato al convegno Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Braga, Portugal nel 13-16 ottobre 2006) [10.1007/978-3-540-71209-1_29].

Abstraction Refinement of Linear Programs with Arrays

BENERECETTI, MASSIMO;
2007

Abstract

In previous work we presented a model checking procedure for linear programs, i.e. programs in which variables range over a numeric domain and expressions involve linear combinations of the variables. In this paper we lift our model checking procedure for linear programs to deal with arrays via iterative abstraction refinement. While most approaches are based on predicate abstraction and therefore the abstraction is relative to sets of predicates, in our approach the abstraction is relative to sets of variables and array indexes, and the abstract program can express complex correlations between program variables and array elements. Thus, while arrays are problematic for most of the approaches based on predicate abstraction, our approach treats them in a precise way.This is an important feature as arrays are ubiquitous in programming. We provide a detailed account of both the abstraction and the refinement processes, discuss their implementation in the eureka tool, and present experimental results that confirm the effectiveness of our approach on a number of programs of interest.
2007
3540712089
Abstraction Refinement of Linear Programs with Arrays / Armando, A; Benerecetti, Massimo; Mantovani, J.. - STAMPA. - LNCS 4424:(2007), pp. 373-388. (Intervento presentato al convegno Tools and Algorithms for the Construction and Analysis of Systems tenutosi a Braga, Portugal nel 13-16 ottobre 2006) [10.1007/978-3-540-71209-1_29].
File in questo prodotto:
File Dimensione Formato  
Abs-Ref-Array-TACAS07.pdf

non disponibili

Tipologia: Documento in Post-print
Licenza: Accesso privato/ristretto
Dimensione 511.24 kB
Formato Adobe PDF
511.24 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: https://hdl.handle.net/11588/116773
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 10
  • ???jsp.display-item.citation.isi??? 6
social impact