Abstract FR:

Une analyse statique est une methode permettant de determiner des informations susceptibles d'etre utilisees par un compilateur a des fins d'optimisation. L'interpretation abstraite est un cadre theorique d'analyse de programmes permettant de determiner des proprietes d'invariance des variables manipulees par ces programmes, c'est-a-dire des proprietes des variables vraies lors de toutes les executions possibles du programme analyse. Cette these fournit un cadre et des domaines d'analyse des langages logiques avec contraintes, permettant le calcul de types recursifs tres precis et de developper des analyses modulaires, tout en garantissant des temps de calcul raisonnables ; d'autre part, elle exhibe les liens qui existent entre l'interpretation abstraite et les approches de l'analyse fondees sur les grammaires attribuees, et generalise les techniques connues d'analyse du test d'occurrence en prolog, tout en en donnant les conditions de faisabilite. L'idee de base de ces contributions est venue de la comparaison entre programmes logiques avec contraintes et grammaires, et en particulier de la separation que l'on peut faire entre un squelette c'est a dire un arbre d'appel ou de derivation et son ensemble de contraintes associe represente par les equations semantiques entre occurrences d'attributs d'une grammaire attribuee