Amphi 22, rez-de-chaussée de l'UFR IMAG (bat F)
21 February 2013 - 14h00
Static Analysis of Programs Manipulating Arrays (Phd Defense)
by Valentin Perrelle from UJF / Verimag
Abstract: Static analysis is key area in compilation, optimization and software validation. The complex data structures (arrays, dynamic lists, graphs, ...) are ubiquitous in programs, and can be challenging, because they can be large or of unbounded size and accesses are computed. (through indexing or indirections)
Whereas the verification of the validity of the array accesses was one of the initial motivations of abstract interpretation, the discovery of properties about array contents was only adressed recently. Most of the analyses of array contents are based on a partitioning of the arrays. Then, they try to discover properties about each fragment of this partition.
The choice of this partition is a difficult problem and each method have its flaw. Moreover, classical representations of array partitions induce an exponential complexity for these analyzes.
In this thesis, we generalize the concept of array partitioning into the concept of fragmentation which allow overlapping fragments, handling potentially empty fragments and selecting specialized relations. On the other hand, we propose an abstraction of these fragmentations in terms of graphs called slices diagrams as well as the operations to manipulate them and ensuring a polynomial complexity. Finally, we propose a new criterion to compute a semantic fragmentation inspired by the existing ones which attempt to correct their flaws. These methods have been implemented in a static analyzer. Experimentations shows that the analyzer can efficiently and precisly prove some challenging exemples in the field of static analysis of programs manipulating arrays.
- Ahmed Bouajjani, Professeur, Université Paris Diderot, Rapporteur
- Xavier Rival, Chargé de recherche, LIENS / INRIA Paris-Rocquencourt, Rapporteur
- Bertrand Jeannet, Chargé de recherche, INRIA Rhône-Alpes, Examinateur
- Jean Claude Fernandez, Professeur, Université Joseph Fourier, Examinateur
- Francesco Logozzo, Senior Scientist, Microsoft Research, Examinateur
- Nicolas Halbwachs, Verimag /CNRS, Directeur de Thèse