2004

• Teachers:
  • Prof. Patrick Cousot,
  • Prof. Roberto Giacobazzi,
  • Prof. Francesco Ranzato,
  • Prof. Dave Schmidt
  
  
• Period: June - December, 2004 (20h)


• Goal of the course: The course is intended as a first introduction to abstract interpretation theory and applications. The course will cover the following topics: Abstract domain design, abstract interpretation theory, Galois connection-based abstractions, widening/narrowing fixpoint approximation, abstract model checking, type inference by abstract interpretation, syntax analysis by abstract interpretation, software watermarking by abstract interpretation, program transformation, implementations of static analysis: trace generation, collecting semantics, data-flow analysis, typing systems, big-step-semantics analysis, data-flow analysis as model checking of abstract interpretations, logics for static analysis: abstract assertion checking; predicate abstraction; ``state logics'' and ``trace logics''; abstraction of linear-time to branching-time logic, logical relations and logics for under- and over-approximation.


• Course material: Cousot's part and slides (8h), Dave's slides (6h): Talk 1.1, Talk 1.2, Talk 1.3, Talk 2.1, Talk 2.2, ...other material is coming!!!


• Tutor: Roberto Giacobazzi


• Exam: A seminar presenting a relevant paper on the suject


• Specials:
  • A light introduction to Abstract Interpretation by P. Cousot
  • Giaco's research interests