Amphi 22, rez-de-chaussée de l'UFR IMAG (bat F)
21 février 2013 - 14h00
Analyse Statique de Programmes Manipulant des Tableaux (Phd Defense)
par Valentin Perrelle de UJF / Verimag
Résumé : L’analyse statique de programmes est un domaine crucial en compilation, en optimisation, et en validation de logiciels. Les structures de données complexes (tableaux, listes, graphes,...), omniprésentes dans les programmes, posent des problèmes difficiles, du fait qu’elles représentent des ensembles de données de taille importante ou inconnue, et que l’adressage des données dans ces ensembles est calculé (indexation, indirection).
Si la vérification de la validité des accès aux tableaux a été l'une des motivations initiales de l'interprétation abstraite, la recherche de propriétés concernant le contenu des tableaux est quant à lui un sujet récent. La plupart des travaux sur le sujet reposent sur un partitionnement des tableaux. On est ainsi amenés à considérer un certain nombre de fragments de tableau desquels on cherche à trouver des propriétés.
Le choix de cette partition est un problème difficile et chacune des méthodes proposées peut être mise en défaut. Par ailleurs, les représentations classiques des partitions de tableau donnent à ces analyses une complexité exponentielle.
Nous proposons d'une part de généraliser le concept de partitionnement de tableau à celui de fragmentation permettant à la fois le chevauchement des fragments, la manipulation de fragments potentiellement vides et la sélection de relations spécialisées. D'autre part, nous proposons une abstraction de ces fragmentations en terme de graphes appelés Diagrammes de tranches ainsi que les opérations pour les manipuler et assurant une complexité polynomiale à l'analyse. Enfin, nous proposons un nouveau critère de fragmentation sémantique inspiré de ceux de la littérature et tentant d'en corriger les défauts. Ces méthodes ont été implémentées dans un analyseur statique. L'expérimentation démontre qu'elles peuvent analyser avec efficacité et précision un certain nombre d'exemples constituant des défis de l'analyse statique de programmes manipulant des tableaux.
Jury:
- 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
