• Lesson 1: Motivations and Informal Introduction (Tuesday, August 31 2004, 10:00—11: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 (Tuesday, August 31 2004, 11:20—13:00, 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) (Wednesday, September 1^st, 10:00—13:00, 180mn) [1/1, 2/1, 4/1]:
  • Informal summary of previous episodes (30 mn);
  • Application to model checking (30 mn);
  • Application to type inference (30 mn);
  • Fixpoint approximation with convergence acceleration by widening/narrowing (20 mn);
  • Application to static interval analysis (30 mn);
  • More expressive numerical abstract domains (10 mn);
  • Questions (5 mn).
• Lesson 4: A Bouquet of Applications (continued) (Thursday, September 2^nd, 15:00—17:00, 120mn) [1/1, 2/1, 4/1]).
  • Application to the static analysis of critical real-time synchronous embedded software (25 mn).
  • Application to syntax analysis (30 mn);
  • Application to predicate abstraction (5 mn);
  • Application to generic predicate abstraction (30 mn);
  • Software watermarking (30 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{Cousot04-Verona}
P{.} Cousot.
\newblock Abstract Interpretation.
\newblock \emph{Ph.D.\ course on Static Analysis},
          Dipartimento di Informatica, Universit\`a degli Studi di Verona, 
          Italy, 31 August-- 2 September, 2004. 

@unpublished{Cousot04-Verona,
   author = {P{.} Cousot},
   title  = {Abstract Interpretation},
   note = {\emph{Ph.D.\ course on Static Analysis},
           Dipartimento di Informatica, Universit\`a degli Studi di Verona, 
           Italy, 31 August-- 2 September, 2004},
}