Cours au M.P.R.I. (droits d'auteur) / Lectures at the M.P.R.I. (copyright notice)

« Interprétation abstraite : application à la vérification et à l'analyse statique »
« Abstract interpretation: application to verification and static analysis »
(M.P.R.I. M2 2.6), année/year 2011/12

Présentation du cours

Plan du cours/Syllabus

Les notions de preuves et de définitions récursives ont été survolées lors du premier cours, et sont des prérequis.
1. Introduction à l'analyse statique par interprétation abstraite
   • Séance 1 du Vendredi 23 septembre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     An Informal Introduction to static analysis and verification by Abstract Interpretation, Fixpoints of increasing maps on posets (part 1), et Program properties.
          On pourra également consulter un cours introductif à l'interprétation abstraite au Collège de France et les notes de cours du MIT.
          Pour compiler et exécuter les programmes OCaml présentés dans ce cours 1 (.tgz, .zip), voir caml.inria.fr, une introduction à OCaml, et le manuel du langage OCaml.

   • Séance 2 du Vendredi 30 septembre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Ordres partiels, Points fixes (part 2), Calcul itératif (chaotique, asynchrone) de points fixes dans les domaines finis, Points fixes et définitions inductives, Approximation itérative de points fixes dans les domains infinis.

2. Sémantique
   • Séance 3 du Vendredi 7 octobre 2010, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Syntaxe, Sémantique de transition, Sémantique de traces transitionelle, définition par extension et par point fixe, Sémantique de traces structurelle, Collecting semantics.

3. Property abstraction

   • Séance 4 du Vendredi 14 octobre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Trace abstraction, State abstraction, Numerical abstraction (part 1).

   • Pas de cours le Vendredi 21 octobre 2011 ,

   • Séance 5 du Vendredi 28 octobre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Numerical abstraction (part 2), Best abstraction (part 1).

   • Pas de cours le Vendredi 1^er novembre 2011,

   • Pas de cours le Vendredi 11 novembre 2011,

   • Séance 6 du Vendredi 18 novembre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Best abstraction (part 2), Program specification, Good abstraction.

4. Transformer abstraction

   • Séance 7 du Vendredi 25 novembre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Abstract transformers,

5. Fixpoint abstraction
   Best fixpoint abstraction, Proof of program properties (part 1), (part 2).
   • Séance 9 du Vendredi 9 décembre 2011, 8h45-11h45 (salle U/V, ENS), Patrick Cousot:
     Good fixpoint abstraction, Reduced product, Refinement by completion.

6. Memory abstraction
   • Séance 10 du Vendredi 16 décembre 2011, 8h45-11h45 (salle U/V, ENS), Xavier Rival:
     Abstraction of memory states

   • Séance 11 du Vendredi 6 janvier 2012, 8h45-11h45 (salle U/V, ENS), Xavier Rival:
     Shape analysis based on separation logic

7. Application to system biology
   • Séances 12 du Vendredi 13 janvier 2012 et 13 du Vendredi 20 janvier 2011, 8h45-11h45 (salle U/V, ENS), Jérôme Feret:
     Abstract interpretation of protein-protein interactions networks, additional material, software and references are available here

8. Numerical abstractions
   • Séance 14 du Vendredi 27 janvier 2012, 8h45-11h45 (salle U/V, ENS), Antoine Miné:
     Numerical abstract domains (part 1)

   • Séance 15 du Vendredi 3 février 2012, 8h45-11h45 (salle U/V, ENS), Antoine Miné:
     Numerical abstract domains (part 2)

Examens/Exams 2011/2012

• Séance 8 du Vendredi 2 décembre 2010, 8h45-11h45 (salle U/V, ENS), Patrick Cousot, Examen partiel (écrit) : Sujet écrit et corrigé .

• Examen final (oral) le Vendredi 9 mars 2012 (salle U/V, ENS). Une liste d'articles de recherche sera proposée plusieurs semaines à l'avance. Il faudra en choisir un, le présenter oralement avec des transparents (20mn) et répondre aux questions d'un jury (10mn) sur l'article et le cours. Les horaires seront fixés individuellement.

Examens des années précédentes/Previous exams

• Examen partiel du 26 novembre 2010: Sujet écrit, Corrigé
• Examen partiel du 20 novembre 2009: Sujet écrit, Corrigé
• Examen partiel du 23 novembre 2007: Sujet écrit, Corrigé
• Examen partiel du 17 novembre 2006: Sujet écrit, Corrigé
• Examen partiel du 02 décembre 2005: Sujet écrit, Corrigé

Propositions de sujets de stages/interships

• Stages proposés dans l'équipe « Interprétation abstraite et sémantique » (ABSTRACTION) du département d'Informatique de l'École normale supérieure/CNRS/INRIA :
  • Domaine Abstrait pour l'Analyse de Structures Dynamiques : Définition d'un Opérateur de Réduction, Xavier Rival, ENS
  • Analyse Statique de Programme Manipulant des Structures Complexes avec Partage, Xavier Rival, ENS