A simple abstraction of arrays and maps by program translation

David Monniaux; Francesco Alberti

doi:10.1007/978-3-662-48288-9_13

A simple abstraction of arrays and maps by program translation

David Monniaux, Francesco Alberti

IRCCS Ospedale San Raffaele

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.

Original language	English
Title of host publication	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Publisher	Springer Verlag
Pages	217-234
Number of pages	18
Volume	9291
ISBN (Print)	9783662482872
DOIs	https://doi.org/10.1007/978-3-662-48288-9_13
Publication status	Published - 2015
Event	22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France Duration: Sep 9 2015 → Sep 11 2015

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	9291
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Other

Other	22nd International Static Analysis Symposium, SAS 2015
Country/Territory	France
City	Saint-Malo
Period	9/9/15 → 9/11/15

ASJC Scopus subject areas

Computer Science(all)
Theoretical Computer Science

Access to Document

10.1007/978-3-662-48288-9_13

Cite this

Monniaux, D., & Alberti, F. (2015). A simple abstraction of arrays and maps by program translation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9291, pp. 217-234). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291). Springer Verlag. https://doi.org/10.1007/978-3-662-48288-9_13

A simple abstraction of arrays and maps by program translation. / Monniaux, David; Alberti, Francesco.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9291 Springer Verlag, 2015. p. 217-234 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9291).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Monniaux, D & Alberti, F 2015, A simple abstraction of arrays and maps by program translation. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 9291, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9291, Springer Verlag, pp. 217-234, 22nd International Static Analysis Symposium, SAS 2015, Saint-Malo, France, 9/9/15. https://doi.org/10.1007/978-3-662-48288-9_13

Monniaux D, Alberti F. A simple abstraction of arrays and maps by program translation. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9291. Springer Verlag. 2015. p. 217-234. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-662-48288-9_13

Monniaux, David ; Alberti, Francesco. / A simple abstraction of arrays and maps by program translation. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 9291 Springer Verlag, 2015. pp. 217-234 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2b1b3cdb5d8a423fa8ea7978a298f290,

title = "A simple abstraction of arrays and maps by program translation",

abstract = "We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.",

author = "David Monniaux and Francesco Alberti",

year = "2015",

doi = "10.1007/978-3-662-48288-9_13",

language = "English",

isbn = "9783662482872",

volume = "9291",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "217--234",

booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

note = "22nd International Static Analysis Symposium, SAS 2015 ; Conference date: 09-09-2015 Through 11-09-2015",

}

TY - GEN

T1 - A simple abstraction of arrays and maps by program translation

AU - Monniaux, David

AU - Alberti, Francesco

PY - 2015

Y1 - 2015

N2 - We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.

AB - We present an approach for the static analysis of programs handling arrays, with a Galois connection between the semantics of the array program and semantics of purely scalar operations. The simplest way to implement it is by automatic, syntactic transformation of the array program into a scalar program followed analysis of the scalar program with any static analysis technique (abstract interpretation, acceleration, predicate abstraction,.). The scalars invariants thus obtained are translated back onto the original program as universally quantified array invariants. We illustrate our approach on a variety of examples, leading to the “Dutch flag” algorithm.

UR - http://www.scopus.com/inward/record.url?scp=84946096377&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84946096377&partnerID=8YFLogxK

U2 - 10.1007/978-3-662-48288-9_13

DO - 10.1007/978-3-662-48288-9_13

M3 - Conference contribution

AN - SCOPUS:84946096377

SN - 9783662482872

VL - 9291

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 217

EP - 234

BT - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

PB - Springer Verlag

T2 - 22nd International Static Analysis Symposium, SAS 2015

Y2 - 9 September 2015 through 11 September 2015

ER -

A simple abstraction of arrays and maps by program translation

Abstract

Publication series

Other

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this