I will be presesting the paper “Discovering Properties about Arrays in Simple Programs” by Nicolas Halbwachs, Mathias Péron, from Verimag (France).

Array bound checking and array dependency analysis (for parallelization) have been widely studied. However, there are much less results about analyzing properties of array contents. In this paper, we propose a way of using abstract interpretation for discovering properties about array contents in some restricted cases: one-dimensional arrays, traversed by simple “for” loops. The basic idea consists in partitioning arrays into symbolic intervals (e.g., [1, i−1], [i, i], [i + 1, n]), and in associating with each such interval I and each array A an abstract variable A_I ; the new idea is to consider relational abstract properties P(A_I , B_I , …) about these abstract variables, and to interpret such a property pointwise on the interval I: for all i in I, P(A[i], B[i], …). The abstract semantics of our simple programs according to these abstract properties has been defined and implemented in a prototype tool. The method is able, for instance, to discover that the result of an insertion sort is a sorted array, or that, in an array traversal guarded by a “sentinel”, the index stays within the bounds.