Qui suis-je ?
Je suis actuellement en fin troisième année de thèse en informatique à
l'Irisa, au sein de l'équipe Lande. Cette thèse est encadrée par
Mireille
Ducassé et Arnaud Gotlieb et financée par une bourse ministérielle. Je suis actuellement en rédaction de thèse. Voici déjà le titre ainsi qu' un résumé de mes travaux de thèse.
Ma thèse
Utilisation de techniques d'interprétation abstraite sur les polyèdres pour le test à base de contraintes
Le test de programmes basé sur les contraintes transforme le problème
de génération de cas de test en un problème de résolution de
contraintes. Les solutions du système de contraintes générés sont des
cas de test pour le programme. Dans mes travaux, les contraintes
générées modélisent des instructions d'un langage de programmation
impératif, y compris des conditionnelles ou des boucles. La résolution
de ces contraintes est basée sur le principe de propagation. Chaque
contrainte est donc munie d'un algorithme qui permet de déduire de
l'information concernant les solutions de cette contrainte. Dans le
cas d'instructions complexes telles que les boucles, l'algorithme de
propagation doit approximer le comportement de la boucle.
L'interprétation abstraite de programmes est un domaine de
recherche qui vise à approximer le comportement des programmes. Dans
ma thèse, j'ai utilisé les deux idées principales de l'interprétation
abstraite pour obtenir des algorithmes de propagation puissants:
|
|  Le principe d'approximation statique permet de réfléchir sur un
domaine de valeurs abstrait au lieu de manipuler des valeurs
concrètes. Dans ce cadre, j'ai utilisé le domaine abstrait des
polyèdres pour approximer les contraintes issues des programmes
impératifs. En pratique, un solveur linéaire coopère dynamiquement
avec un solveur à domaines finis pour accélérer la résolution des
contraintes. |
|
| Le principe d'approximation dynamique permet de calculer une
sur-approximation du résultat de calculs itératifs infinis ou très
longs. J'ai fait de cette technique la base de l'algorithme de
propagation des contraintes modélisant des boucles. |
L'intégration de ces deux techniques d'interprétation abstraite au
sein d'un solveur de contraintes à domains finis permet d'accélérer de
manière significative la résolution des systèmes de contraintes issus
des programmes impératifs. J'ai implémenté un outil de génération de
cas de test qui montre l'intérêt de cette approche.
Contact
| Adresse | : |
Irisa
Projet Lande
Campus de Beaulieu
35042 Rennes Cedex
France |
| |
|
Dernières modifications : Juillet 2007