Un analyseur statique est un outil entièrement automatisé permettant de prédire les comportements à l'exécution d'un programme par le seul examen de son texte. Il est utilisé pour répondre automatiquement à des questions sur les comportements possibles des programmes à l'exécution. Pour ce faire, l'idée de base qui nous a guidé pour concevoir l'interprétation abstraite est qu'il suffit de considérer une approximation pertinente de la sémantique des programmes. Cette sémantique décrit formellement tous les comportements possibles d'un programme. C'est un modèle mathématique qui représente les structures créées par le programme ainsi que leur évolution au cours de toutes les exécutions possibles du programme. Des théorèmes généraux d'indécidabilité montrent qu'il n'est pas possible de calculer automatiquement et de manière exacte la sémantique d'un programme. L'interprétation abstraite permet de résoudre ce problème en se restreignant à des sous-ensembles pertinents des informations observées sur les comportements des programmes. 

        Dans une première partie, on expliquera les principes de l'interprétation abstraite c'est-à-dire de la théorie permettant de construire des analyseurs statiques cohérents et fiables à partir de la sémantique d'un programme et d'une spécification des propriétés observables des comportements du programme. Elle a de nombreux champs d'application comme la conception de sémantiques, le typage, le model-checking abstrait et l'analyse statique qui fait l'objet de ce séminaire. 

        Dans une deuxième partie, nous abordons deux applications à l'analyse statique. La première concerne la recherche d'erreurs à l'exécution. Il s'agit de déterminer quelles sont les erreurs comme le défaut d'initialisation, les dépassements de capacité (par exemple le dépassement des bornes de tableaux), les défauts de synchronisation, les pointeurs pendants, etc. qui sont certaines, potentielles ou impossibles à l'exécution.
        La deuxième application concerne le test abstrait. Il s'agit de déterminer des conditions nécessaires pour qu'une spécification donnée par le programmeur soit satisfaite, ce qui permet de rechercher les erreurs.