I am interested in static analysis of numerical programs, in particular the analysis of arrays contents. I have a grant of CNRS to carry out this work in the synchronous team of Verimag laboratory, under the supervision of Nicolas Halbwachs.
We proposed [PLDI'08] a new static
analysis by means of abstract interpretation to discover properties
about array contents.
The analysis is parameterized by two abstract domains: a numerical one to handle
properties about scalar variables that index the arrays; an other one to handle array contents properties,
which are not necessary about numerics. Relational array-cell properties can be expressed:
∀ k ∈ [2,n], A[k] ≥ A[k-1].
Although the class of programs on which the analysis will give good results is restricted (loops on variables that index arrays can only progress by unit steps), interesting algorithms fall into the class: insertion sort, segmentation phase of quicksort, sentinel based algorithms, etc.
We also introduced [VMCAI'07] a new numerical abstract domain handling disequality constraints between pair of variables. Those invariants (x ≠ y, x ≠ 0) are coupled with zones in order to discover non-trivial invariants (x > z &ge y ⇒ x ≠ y). Algorithms and representation of the domain are based on DBMs one, leading us to call it disequalites Difference-Bound Matrices (dDBM).
To appear soon.
During my studies at ENS of Lyon I worked on ad hoc networks, at INRIA and Trinity College of Dublin