A simple abstraction of arrays and maps by program translation

David Monniaux, Francesco Alberti

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
PublisherSpringer Verlag
Pages217-234
Number of pages18
Volume9291
ISBN (Print)9783662482872
DOIs
Publication statusPublished - 2015
Event22nd International Static Analysis Symposium, SAS 2015 - Saint-Malo, France
Duration: Sep 9 2015Sep 11 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume9291
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other22nd International Static Analysis Symposium, SAS 2015
CountryFrance
CitySaint-Malo
Period9/9/159/11/15

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint Dive into the research topics of 'A simple abstraction of arrays and maps by program translation'. Together they form a unique fingerprint.

  • 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