3. Domaines de recherche
L'équipe étudie la sémantique et
l'interprétation abstraite, un domaine de recherche qu'elle a
créé. Les principales applications pratiques concernent
l'analyse statique.
Sémantique
En informatique, la sémantique d'un langage fournit pour tout
programme écrit dans ce langage un modèle mathématique
formel de tous les comportements possibles d'un système informatique
exécutant ce programme en interaction avec un environnement
quelconque.
Toutes les questions intéressantes relatives à la
sémantique d'un programme sont indécidables,
c'est-à-dire qu'aucun ordinateur ne peut toujours y répondre
en un temps fini.
Interprétation abstraite
L'interprétation abstraite est une théorie de l'approximation
de sémantiques de langages (de programmation ou de
spécification). Elle permet de formaliser l'idée qu'une
sémantique est plus ou moins précise selon le niveau
d'observation auquel on se place. Si l'approximation est suffisamment
grossière, l'abstraction d'une sémantique peut permettre d'en
donner une version moins précise mais calculable. La perte
d'information ne permet pas de répondre à toutes les
questions mais toutes les réponses données par calcul
effectif de la sémantique abstraite sont toujours justes.
La présentation informelle Abstract Interpretation in a Nutshell
est une introduction
rapide et informelle à la théorie.
Analyse statique
L'analyse statique utilise l'interprétation abstraite pour
dériver de la sémantique standard une sémantique
calculable par l'ordinateur. De ce fait un ordinateur est capable
d'analyser le comportement de programmes et de logiciels avant même
de les exécuter. Ceci est essentiel, par exemple dans les
systèmes informatiques critiques (avions, fusées, centrales
nucléaires) pour découvrir les erreurs (qui ont
échappé aux programmeurs) avant qu'elles ne produisent des
catastrophes!
