• Langue : Français
• Discipline : Informatique
• Identifiant : Inconnu
• Type de thèse : Doctorat
• Date de soutenance : 01/01/1994

Résumé en langue originale

L'interpretation abstraite est une technique d'analyse statique qui permet d'analyser le comportement dynamique d'un programme. Dans cette these, nous proposons un modele generique d'interpretation abstraite applique a la programmation logique avec contraintes. Ce modele est compose d'une phase d'extension du domaine suivie d'une phase d'abstraction du calcul. L'extension du domaine consiste a integrer de nouvelles contraints au domaine d'un clp-langage et l'abstraction du calcul consiste a forcer la terminaison de la resolution old via l'utilisation conjuguee d'une technique de tabulation et d'operateurs de widening. Nous illustrons ce modele avec une application non triviale portant sur l'inference de types en polog. Pour cette analyse, l'extension du domaine correspond a l'integration de contraintes ensemblistes. Ainsi, les contraintes du langage obtenu portent a la fois sur les termes (ou arbres) finis et sur les ensembles. L'interet de cette combinaison est que les contraints sur les termes permettent de coder les dependances entre les variables et que les contraintes ensemblistes permettent de coder les structurs recursives et non deterministes.