• Lesson 1: Motivations and Informal Introduction (Monday, March 3 2003, 10:50—12:20, 90mn):
  • 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 (Tuesday, March 4, 16:10—17:30, 80mn):
  • 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: Application to Static Analysis (Thursday, March 6, 09:00—10:30, 90mn):
  • Application to predicate abstraction (10 mn);
  • Application to model checking (20 mn);
  • Application to type inference (20 mn);
  • Fixpoint approximation with convergence acceleration by widening/narrowing (10 mn);
  • Application to static interval analysis (10 mn);
  • More expressive numerical abstract domains (5 mn);
  • Application to the static analysis of critical real-time synchronous embedded software (10 mn).
  • Exercices & questions (5 mn).

• 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-EWSCS}
P{.} Cousot.
\newblock An Introduction to Abstract Interpretation, EWSCS 2003 course.
\newblock \emph{8^{\mathrm{th}} Estonian Winter School in Computer Science
         (EWSCS) / VIII Eesti Arvutiteaduse Talvekool (EATTK)} Palmse, Estonia, March
         2--7, 2002.

@unpublished{Cousot03-EWSCS,
   author = {P{.} Cousot},
   title  = {An Introduction to Abstract Interpretation, EWSCS 2003 course},
   note   = {\emph{8^{\mathrm{th}} Estonian Winter School in Computer Science
            (EWSCS) / VIII Eesti Arvutiteaduse Talvekool (EATTK)} Palmse, Estonia, March
            2--7, 2002},
}