• Lesson 1: Motivations and Informal Introduction (Friday, May 27 2004, 9:00—10:30, 90mn) [1/1, 2/1, 4/1]:
  • Motivations for formal methods (10 mn);
  • On formal methods and computer-aided verification (10 mn);
  • Motivations for Abstract Interpretation (5 mn);
  • Informal introduction to Abstract Interpretation (using a graphical language, 55 mn);
  • The future of software verification (5 mn);
  • Exercices & questions (5 mn).
• Lesson 2: Elements of Abstract Interpretation Theory (Friday, May 27 2004, 11:00—12:30, 90mn) [1/1, 2/1, 4/1]:
  • What is abstract interpretation? (5 mn)
  • A short introduction to abstract interpretation theory (55 mn): objects, properties, concrete and abstract properties, minimal approximations, best approximations, Moore families, closure operators, Galois connections, abstract domains, function abstraction, fixpoints, fixpoint approximation and exact abstraction, soundness, completeness, combination of abtract domains, iterative fixpoint approximation with convergence acceleration by widening/narrowing, completion of abstract domains, local image and domain completion, the lattice of Abstract Interpretations;
  • Application to reachability (10 mn).
  • Reachability with structural induction for programming languages (5 mn).
  • Exercices & questions (5 mn).
• Lesson 3: A Bouquet of Applications (to Static Program Analysis) (Friday, May 27, 14:00—15:30, & 16:00—17:15, 165mn) [1/1, 2/1, 4/1]:
  • Application to predicate abstraction (5 mn);
  • Application to model checking (20 mn);
  • Application to type inference (10 mn);
  • Fixpoint approximation with convergence acceleration by widening/narrowing (40 mn);
  • Application to static interval analysis (30 mn);
  • More expressive numerical abstract domains (10 mn);
  • Application to the static analysis of critical real-time synchronous embedded software (45 mn).
  • Questions (5 mn).
• Not enough time was left for the last course (on application to syntax analysis and generic predicate abstraction [1/1, 2/1, 4/1]).

• P. Cousot. Semantic foundations of program analysis.
  In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, chapter 10, pages 303—342. Prentice-Hall, Inc., Englewood Cliffs, New Jersey, USA, 1981.
  
• P. Cousot. Abstract interpretation based formal methods and future challenges, invited paper.
  In R. Wilhelm, editor, « Informatics — 10 Years Back, 10 Years Ahead », volume 2000 of Lecture Notes in Computer Science, pages 138--156. Springer-Verlag, 2000.

\bibitem{Cousot04-EJCP}
P{.} Cousot.
\newblock Abstract Interpretation, EJCP'2004 course.
\newblock \emph{EJCP'2004, \'Ecole jeunes Chercheurs en Programmation},
          \'Ecole des Mines de Nantes, France, 24 May -- 4 June, 2004.

@unpublished{Cousot04-EJCP,
   author = {P{.} Cousot},
   title  = {Abstract Interpretation, EJCP'2004 course},
   note = {\emph{EJCP'2004, \'Ecole jeunes Chercheurs en Programmation},
           \'Ecole des Mines de Nantes, France, 24 May -- 4 June, 2004},
}