Sémantique et interprétation abstraite

Responsable : Patrick Cousot

• La production de logiciels fiables et performants passe en partie par l'automatisation de leur construction. Pour atteindre cet objectif, il est indispensable d'étudier les programmes en tant qu'objets mathématiques.
  • Nous adoptons un point de vue sémantique (1), pour définir la nature des calculs effectués par les programmes et préciser les traitements déductifs rigoureux qui permettent de démontrer les propriétés des exécutions de ces programmes.

  • Nous adoptons également le point de vue calculatoire de l'interprétation abstraite (2): les programmes peuvent faire l'objet de calculs sur ordinateur afin de découvrir automatiquement leurs propriétés sémantiques. Ces programmes de manipulation sémantique de programmes doivent eux-mêmes faire l'objet d'une réflexion voire d'une construction automatique, qui sont le sujet de notre travail sur l'analyse sémantique de programmes par interprétation abstraite.

• Nos différents thèmes de recherche concernent :
  • La sémantique des langages de programmation :
    • modèles des calculs séquentiels, parallèles, distribu;és, temps réél, probabilistes, ... ;
    • méthodes de définition de la sémantique des programmes et plus généralement des systèmes informatiques ;
    • étude des correspondances entre sémantiques ;
    • méthodes de preuve de propriétés sémantiques de programmes ;
    • étude de la correction et de la complétude de ces méthodes de preuve de programmes relatives à une sémantique ;
    • etc.

  • L'analyse sémantique des programmes par interprétation abstraite :
    • étude des techniques d'approximation discrète des domaines de calcul et utilisation pour l'approximation de sémantiques ;
    • étude de structures mathématiques discrètes permettant d'exprimer les propriétés sémantiques approchées des objets manipulés par les programmes (comme par exemple les relations linéaires d'égalité, d'inégalité ou de congruence entre valeurs des variables numériques ou bien les propriétés de partage des structures de données non numériques) ;
    • étude des systèmes de types, vérification et inférence de types ;
    • étude de l'interprétation abstraite de structures de contrôle des programmes (fonctions d'ordre supérieur dans les langages fonctionnels, retour-arrière dans les programmes logiques, mécanismes de communication et de synchronisation dans les programmes parallèles, etc) ;
    • étude de la résolution itérative et approchée de systèmes d'équations de point fixe sur des ensembles ordonnés discrets, en particulier les méthodes de simplification des équations et d'accélération de la convergence ;
    • etc.

  • Les applications concernent :
    • les outils d'aide à la mise au point des programmes ;
    • la production automatique de tests ;
    • l'optimisation pendant la compilation ;
    • la transformation de programmes pour les machines vectorielles, massivement parallèles ou leur distribution sur des ordinateurs répartis ;
    • les outils de vérification de programmes ;
    que ce soit pour les programmes impératifs, fonctionnels, logiques, parallèles, orientés-objets, etc.

  • Bibliographie sur l'interprétation abstraite.