Non-disjunctive numerical domain for array predicate abstraction

Abstract. 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 rela-tions 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 bench-marks. Our approach is sufficiently robust to handle programs traversing arrays and matrices in various ways.