Table of Contents
Interprétation abstraite : application à la vérification et à l'analyses statique (48h, 6 ECTS)Responsable : Antoine Miné OrganisationPour 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
ObjectifsL'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
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
|