Abstract FR:

Le but de cette these est le developpement d'une structure de donnees representant les ensembles eventuellement infinis d'arbres eventuellement infinis, et ce dans le cadre de l'interpretation abstraite, en utilisant les possibilites d'approximations offertes par cette technique. La these se preoccupe de l'efficacite de la representation et donne les algorithmes permettant de manipuler ces structures. Les structures de donnees developpees dans cette these mettent en uvre un principe de partage des structures isomorphes permettant l'efficacite des algorithmes et la compacite de la representation. Ce principe est facile a appliquer dans le cadre de structures sans cycle, qui correspondent aux arbres finis. Le cas des structures avec cycles est traite dans la these. Il est utilise dans toutes les representations de donnees infinies regulieres. Dans la representation des ensembles d'arbres, le principe de partage met en evidence l'aspect relationnel des ensembles. Ces relations pouvant etre infinies, des representations de relations infinies ont ete developpees. La plus expressive de ces representations est une extension des diagrammes de decision binaires (bdds) qui ont fait leur preuve dans la representation des relations finies. De nouvelles classes de relations infinies ont ete definies. Ces nouvelles representations peuvent etre utiles en elles-memes pour l'analyse statique de programmes. La structure de donnees representant les ensembles d'arbres a un grand pouvoir expressif : elle permet de representer des arbres infinis avec des proprietes d'equite sur leurs labels, des ensembles representables par automates d'arbres avec contrainte entre freres, ou des ensembles de la forme f(a n, b n, c n). Des algorithmes permettant d'orienter la recherche d'approximations sont proposes. Enfin, ces structures de donnees sont appliquees a des exemples simples d'analyses statiques de programmes.