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 -