Description
Date depot: 1 janvier 1900
Titre: Combinaison de l'interprétation abstraite et de la programmation par contraintes : fondements et applications à l'amélioration de l'analyse de programmes et de la résolution de contraintes
Directeur de thèse:
Antoine MINE (LIP6)
Encadrante :
Charlotte TRUCHET ()
Domaine scientifique: Sciences pour l'ingénieur
Thématique CNRS : Non defini
Resumé:
Le thèse se situe à la frontière de deux domaines : l'interprétation abstraite, qui est une théorie de l’approximation des sémantiques de programmes appliquée à l'analyse statique de la correction des logiciels, et la programmation par contraintes, un cadre de programmation déclarative permettant de résoudre une grande variété de problèmes exprimés en logique du premier ordre.
Inventées puis développées de manière indépendante, ces domaines n'ont a priori ni les mêmes objectifs, ni les mêmes méthodes pour atteindre ces objectifs. En 1997, Krzysztof Apt décèle des liens fondamentaux en interprétant une des notions centrales en programmation par contraintes, les consistances, comme des itérations chaotiques introduites en interprétation abstraite. Dans un travail plus récent, de nature plus pragmatique, Pelleau et al. s’intéressent à importer en programmation par contraintes le concept de domaine numérique abstrait, issu de l’interprétation abstraite
Ces travaux précurseurs sur les liens entre interprétation abstraite et programmation par contraintes laissent de côté plusieurs aspects pourtant critiques de chacun des domaines. Le but de la thèse est de renforcer les liens théoriques entre ces deux domaines, puis d'appliquer ces résultats au transport de méthodes d’un domaine à l'autre, afin de faire bénéficier chaque domaine des apports spécifique et des algorithmes spécialisés développés par l'autre domaine. Le projet mêlera des aspects théoriques et fondamentaux sur les domaines de l'interprétation abstraite et de la programmation par contraintes, ainsi que des aspects appliqués, l’implantation des solutions retenues dans des prototypes et l’expérimentation sur des bancs de tests classiques des deux domaines de recherche.
Doctorant.e: Ziat Ghiles Nacer