Abstract FR:

L'interpretation abstraite est une technique puissante d'analyse semantique qui permet la detection de proprietes dynamiques. Elle repose sur la notion d'abstraction (ou approximation) qui remplace les elements du domaine habituel - dit concret - par ceux du domaine abstrait. Nous presentons une semantique deductive de prolog, qui approche la semantique operationnelle standard et possede une propriete de compositionnalite grace a l'utilisation de l'espace des termes quotiente par la relation de renommage et grace a une decomposition de l'operateur d'unification en deux parties independantes. Puis nous proposons pour cette semantique un interprete abstrait generique, c'est-a-dire qui necessite pour une analyse donnee un nombre tres limite d'informations decrivant le domaine et les operateurs abstraits. Cet interprete est implemente en c, fonctionne avec precision et efficacite, et n'est pas restreint aux treillis abstraits de hauteur finie. Nous utilisons ensuite cet outil pour detecter certaines familles de proprietes, et expliquons comment un compilateur ou un repartiteur de programmes prolog peut tirer parti de telles informations