• Lesson 1: Motivations and Informal Introduction (Thursday, May 29 2003, 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, 60 mn);
  • Exercices & questions (5 mn).
• Lesson 2: Elements of Abstract Interpretation Theory (Thursday, May 29 2003, 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 (15 mn).
  • Exercices & questions (5 mn).
• Lesson 3: A Bouquet of Applications (to Static Program Analysis) (Thursday, May 29, 14:00—15:30, & 16:00—17:30, 180mn) [1/1, 2/1, 4/1]:
  • Application to predicate abstraction (20 mn);
  • Application to model checking (30 mn);
  • Application to type inference (30 mn);
  • Fixpoint approximation with convergence acceleration by widening/narrowing (10 mn);
  • Application to static interval analysis (20 mn);
  • More expressive numerical abstract domains (10 mn);
  • Application to the static analysis of critical real-time synchronous embedded software (30 mn).
  • Questions (30 mn).
• Not enough time was left for the last course (on application to syntax analysis and generic predicate abstraction).

• 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{Cousot03-EJCP}
P{.} Cousot.
\newblock Abstract Interpretation, EJCP'2003 course.
\newblock \emph{EJCP'2003, \'Ecole jeunes Chercheurs en Programmation},
          Aussois, France, March 26 May -- 6 June, 2003.

@unpublished{Cousot03-EJCP,
   author = {P{.} Cousot},
   title  = {Abstract Interpretation, EJCP'2003 course},
   note = {\emph{EJCP'2003, \'Ecole jeunes Chercheurs en Programmation},
           Aussois, France, March 26 May -- 6 June, 2003},
}