Parisian Master of Research in Computer Science
Master Parisien de Recherche en Informatique (MPRI)

Interprétation abstraite : application à la vérification et à l'analyses statique (48h, 6 ECTS)

Responsable : Antoine Miné

Organisation

Pour l'année 2024-2025, le cours a lieu le lundi de 8h45 à 11h45 à l'Université Paris Cité, dans le bâtiment Sophie Germain, en salle 1002.

Il comporte 16 séances.

Les dates précises des cours et le matériel pédagogique sont regroupés sur la page d'organisation du cours.

Dates importantes

  • début des cours : lundi 23 septembre 2024 ;
  • examen écrit à l'issue de la première période : 2 décembre 2024 de 8:45 à 11:45 ;
  • examen oral à l'issue de la deuxième période : à venir.

Objectifs

L'interprétation abstraite est une théorie générale de l'approximation des sémantiques de systèmes dynamiques. Une application importante est la vérification de programmes par construction d'analyses statiques répondant à des questions concernant leur comportement à l'exécution. Ces analyses terminent toujours, sont automatiques (sans interaction avec l'utilisateur), approchées (afin de contourner les problèmes d'indécidabilité et pour assurer l'efficacité) et sûres (par sur-approximation de l'ensemble des comportements).

L'objectif du cours est de présenter la théorie de l'interprétation abstraite ainsi que les instances importantes d'analyses statiques par interprétation abstraite.

À l'issue du cours, l'élève devrait être capable de concevoir une analyse statique, de prouver sa correction et sa terminaison, d'apprécier sa précision et ses limites. Il devrait également être capable de comprendre les articles publiés dans les conférences spécialisées du domaine (telles que SAS et VMCAI) et d'y déceler les abstractions à l'œuvre.

Plan du cours et thèmes abordés

  1. Fondements de l'interprétation abstraite :
    1. bases mathématiques : théorie de l'ordre, théorèmes de points-fixes, correspondances de Galois,
    2. définitions constructives, abstractions et approximations de sémantiques,
    3. hiérarchies de sémantiques et de propriétés : sémantiques de traces et d'état, propriétés de sûreté, de vivacité, d'interférences,
    4. combinaison de domaines abstraits : produits réduits, complétions, partitionnements ;
  2. Exemples de domaines abstraits et d'analyses statiques :
    1. domaines abstraits numériques,
    2. domaines abstraits symboliques,
    3. analyses statiques de mémoire,
    4. analyses statiques de programmes concurrents,
    5. analyses statiques de programmes mobiles,
    6. analyses statiques de systèmes biologiques,
    7. analyses de terminaison,
    8. analyses statiques de réseaux de neurones.

Le cours insiste en particulier sur les points suivants : la construction systématique d'analyses statiques par approximation de sémantiques constructives, l'universalité de la notion d'abstraction, l'intérêt qu'il y a à employer des abstractions infinitaires, la modularité et la réutilisabilité des domaines abstraits, la complémentarité entre les approximations statiques (dues aux domaines) et dynamiques (dues à l'extrapolation des points-fixes).

Équipe pédagogique

J. FeretCRINRIADI
A. MinéPUSULIP6
X. RivalDRINRIADI
C. UrbanCRINRIADI
 
Universités partenaires Université Paris-Diderot
Université Paris-Saclay
ENS Cachan École polytechnique Télécom ParisTech
ENS
Établissements associés Université Pierre-et-Marie-Curie CNRS INRIA CEA