Des analyseurs statiques ont été développés avec succès pour détecter les erreurs d’exécution dans de nombreux langages. Cependant, l’analyse automatique des langages fonctionnels demeure un défi en raison des fonctions récursives, des types de données algébriques récursifs et des fonctions d’ordre supérieur. Les systèmes de types classiques offrent des méthodes compositionnelles qui ne sont, en général, pas suffisamment précises pour prouver l’absence d’erreurs d’exécution telles que les échecs d’assertions. À l’opposé, les méthodes déductives sont plus expressives mais peuvent nécessiter l’intervention de l’utilisateur pour prouver les invariants.
Cette thèse vise à concevoir une analyse statique de valeurs par interprétation abstraite pour un langage fonctionnel pur d’ordre supérieur. Cette analyse fournit une approche sûre et automatique pour découvrir des invariants et prévenir les échecs d’assertions et de filtrage. Nous avons conçu une analyse compositionnelle dite bottom-up : les fonctions sont analysées une seule fois, à leur point de définition, générant un résumé de leur comportement. Ces résumés peuvent être vus comme des relations entrée-sortie exprimées dans des domaines abstraits relationnels. Cette analyse a été implémentée dans la plateforme Mopsa pour un sous-ensemble pur d'OCaml.