TY - GEN
T1 - Non-disjunctive numerical domain for array predicate abstraction
AU - Allamigeon, Xavier
PY - 2008/7/21
Y1 - 2008/7/21
N2 - We present a numerical abstract domain to infer invariants on (a possibly unbounded number of) consecutive array elements using array predicates. It is able to represent and compute affine equality relations over the predicate parameters and the program variables, without using disjunctions or heuristics. It is the cornerstone of a sound static analysis of one- and two-dimensional array manipulation algorithms. The implementation shows very good performance on representative benchmarks. Our approach is sufficiently robust to handle programs traversing arrays and matrices in various ways.
AB - We present a numerical abstract domain to infer invariants on (a possibly unbounded number of) consecutive array elements using array predicates. It is able to represent and compute affine equality relations over the predicate parameters and the program variables, without using disjunctions or heuristics. It is the cornerstone of a sound static analysis of one- and two-dimensional array manipulation algorithms. The implementation shows very good performance on representative benchmarks. Our approach is sufficiently robust to handle programs traversing arrays and matrices in various ways.
UR - https://www.scopus.com/pages/publications/47249147001
U2 - 10.1007/978-3-540-78739-6_14
DO - 10.1007/978-3-540-78739-6_14
M3 - Conference contribution
AN - SCOPUS:47249147001
SN - 3540787380
SN - 9783540787389
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 163
EP - 177
BT - Programming Languages and Systems - 17th European Symposium on Programming, ESOP 2008 - Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2008, Proceedings
T2 - 17th European Symposium on Programming, ESOP 2008
Y2 - 29 March 2008 through 6 April 2008
ER -