[M1R 2012-2013] Analyse de programmes avec types structure complexes


Laboratoire : LIAFA
Equipe : Vérification
Encadrant : Mihaela Sighireanu ( http://www.liafa.univ-paris-diderot.fr/~sighirea )

Contexte scientifique : L'analyse de programmes calcule de façon sûre des propriétés vraies pour toutes les exécutions de programmes. Ces analyses sont à présent utilisés sur des logiciels dont la taille est de plus en plus grande. D'où la difficulté de garder une bonne précision et une bonne complexité (en temps et espace), sachant que les problèmes considérés sont souvent indécidables ou NP-durs.
Une technique pour obtenir une bonne complexité de l'analyse est d'abstraire les parties du programme qui ne sont par intéressantes pour l'analyse afin d'obtenir un programme plus petit, donc plus facile à analyser. Cette technique est connue sur le nom de tranchage (slicing) d'un programme. Appliquée à un programme P, elle permet d'obtenir un autre programme P' plus simple mais qui garde les parties "intéressantes" du programme original P. Par exemple, la tranche de P obtenue en s'intéressant à la valeur de la variable x à la ligne de programme l est donnée par l'ensemble d'instructions du programme P qui peuvent affecter la valeur de x à la ligne l.
La technique de slicing est basée sur le calcul d'un graphe de dépendance des instructions et son parcours (en arrière) en partant de l'instruction intéressante. Plusieurs outils utilisent cette technique pour l'analyse de code C, l'un d'eux étant l'outil Frama-C développé par le CEA.

Sujet : Peu de travaux existent sur le slicing appliqué aux types de données structurés. Il s'agit de considérer pour un type le programme qui utilise uniquement une partie des champs de ce type, si un tel programme existe. Par exemple, pour un type qui a plusieurs champs et un champ récursif next, on peut trancher que la partie de programme qui utilise le champ next afin d'appliquer les outils d'analyse de programmes avec listes dynamiques, comme Celia. Ce type de technique devrait permettre d'augmenter la classe de programmes analysés avec Celia et améliorer ses performances.

Connaissances préalables souhaitées :