Abstract Interpretation
Program analysis by abstract interpretation is a long-standing research topic in the team, aiming at complementing model-checking techniques with analyses able to take into account numerical properties and data structures. During the considered period, these works took place first within the APRON, and now within the new project ASOPT (static analysis and optimisation) of the ANR programme Arpege (2009-11). In 2007, the arrival of David Monniaux, moving from Patrick Cousot’s team at ENS, was of course a very positive event for this theme.
David Merchat’s thesis was devoted to Cartesian factoring of polyhedra in linear relation analysis (LRA). The results were published in FMSD [1].
Verification of Array properties
Such analysis is faced with the problem of aliasing: changing a cell A[i] may silently change A[j], if it happens that i = j. As a consequence, we first proposed an analysis deciding whether, at a given program point, two variables are alway different. This was the subject of Mathias Péron’s master thesis [2] and was published in VMCAI’07 [3].
Then, we considered the automatic discovery of properties involving array contents, and we proposed an analysis for simple programs (handling one-dimensional arrays by simple iteration), which is able, for instance, to discover that the result of an insertion sort procedure is indeed a sorted array. This was published in PLDI’08 [4]. Moreover, we defined an analysis for discovering that an array is a permutation of another array (which, continuing the previous example, terminates the proof of the sorting procedure: not only the result is sorted, but it is a permutation of the initial array).
Exact abstract fixpoint computation and modular analysis
Two well-known weaknesses of most approaches of static program analysis by abstract interpretation are the computation of fixed points using widen- ings (the classical way of enforcing termination in abstract interpretation) and the lack of modularity.
Concerning widening, it is sometimes possible to compute least fixed points or good approximations thereof directly. In the case of LRA (linear relation analysis) we identified many cases of program loops the abstract effect of which can be computed exactly without iterations: in these cases, the analysis is both more precise and more efficient. Moreover, this technique is compatible with the use of widening, and therefore does not restrict the applicability of the analysis. This work took place in the thesis of Laure Gonnord, and was published in SAS’06 [5].
Another approach is to reduce the fixed point problem to a quantifier elimination problem (see POPL’09 paper [6]).
Not only is it possible to exactly solve the least fixed point problem for certain classes of programs and domains, this approach is also modular in the sense that the abstract transfer function of a sub-program can be compiled once and for all. Unfortunately the state of the art in quantifier elimination is not yet satisfactory for this method to scale up well. This led us to work on improvements to quantifier elimination algorithms (see LPAR’08 paper [7]) based on modern SMT-solving techniques. Another promising direction is to use numerical algorithms from operational research, but these, implemented in floating-point, usually do not provide assurance that their results are correct. We therefore researched how certain floating-point algorithms can be safely applied to accelerate some exact constraint computations (see CAV’09 paper [8]).
