Course on Abstract Interpretation
Patrick Cousot
IBM T.J. Watson Research Center — Hawthorne N.Y.

Objective:

Prospective Course Description:

1. Fri Apr 06, 1:30—3:00, Room: GN-F15
   • Lecture 1: An overview of the basic concepts of abstract interpretation
   • This first lecture is a rapid overview, presenting the concepts that will be developped later in the course. The lecture to attend if you come only once. All the misunderstood points will be explained in the rest of the course.
   • Patrick Cousot and Radhia Cousot. “Basic Concepts of Abstract Interpretation.”/ In Building the Information Society, René Jacquard (Ed.), Kluwer Academic Publishers, pp. 359—366, 2004.
2. Wed Apr 11, 3:00—4:30, Room: GN-F15
   • Lecture 2: Set and lattice theory
   • Set and lattice theory formalize the notion of ``program property'' in abstract interpretation
   • B.A. Davey & H.A. Priestley. “Introduction to lattices and order”. Cambridge University Press, 2nd edition, 2002, 298 p.
3. Fri Apr 13, 1:30—3:00, Room: GS-F58
   • Lecture 3: Ordered maps, closures, Galois connections
   • Introduce the mathematical concepts used to define (abstract) property transformers and well as the notion of abstraction.
   • B.A. Davey & H.A. Priestley. “Introduction to lattices and order”. Cambridge University Press, 2nd edition, 2002, 298 p.
4. Tue Apr 17, 3:00—4:30, Room: GS-F58
   • Lecture 4: Fixpoints
   • More mathematical concepts used to define the (abstract) semantics of programming languages.
   • Alfred Tarski (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics 5:2:285—309.
   • Patrick Cousot, Radhia Cousot (1979). Constructive versions of Tarski's fixed point theorems, Pacific Journal of Mathematics. 82:1:43—57.
5. Fri Apr 20, 1:30—3:00, Room: GN-F15
   • Lecture 5: Semantics
   • Inductive definitions, semantics of programming languages at various levels of abstraction (using fixpoint or rule-based definitions).
   • Patrick Cousot & Radhia Cousot. Inductive definitions, semantics and abstract interpretation. In Conference Record of the 19th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Programming Languages, pages 83—94, Albuquerque, NM, January 1992. ACM Press
6. Wed Apr 25, 3:00—4:30, Room: GN-F15
   • Lecture 6: Abstraction
   • The mathematical design of abstract domains.
   • Patrick Cousot & Radhia Cousot. Abstract interpretation frameworks. Journal of Logic and Computation, 2(4):511—547, August 1992.
7. Fri Apr 27, 1:30—3:00, Room: GS-F58
   • Lecture 7: Fixpoint exact and approximate abstraction
   • Foundations of fixpoint-abstraction-based static analysis
   • Patrick Cousot. Semantic foundations of program analysis. In S.S. Muchnick & N.D. Jones (eds), Program Flow Analysis: Theory and Applications, Ch. 10, pages 303—342, Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 1981.
8. Tue May 01, 3:00—4:30, Room: GN-F15
   • Lecture 8: Properties of Widenings & Combination of abstractions
   • Why and how using widenings? The design of static analyzers by combining abstractions.
   • Patrick Cousot & Radhia Cousot. Comparing the Galois connection and widening/narrowing approaches to abstract interpretation. In M. Bruynooghe & M. Wirsing (eds), Programming Language Implementation and Logic Programming, Proceedings of the Fourth International Symposium, PLILP'92, Leuven, Belgium, 13Ñ17 August 1992, Lecture Notes in Computer Science 631, pp. 269—295. Springer, 1992.
9. Fri May 04, 1:30—3:00, Room: GS-F58
   • Lecture 9: Numerical abstractions
   • The static analysis of numerical properties of programs.
   • Antoine Miné. Relational Abstract Domains for the Detection of Floating-Point Run-Time Errors. In European Symposium on Programming (ESOP), 2004, LNCS 2986, Springer, pages 3—17
10. Tue May 08, 3:00—4:30, Room: GN-F15
    • Lecture 10: Symbolic abstractions
    • The static analysis of non-numerical properties of programs.
    • Laurent Mauborgne. An Incremental Unique Representation for Regular Trees. Nordic Journal of Computing, 7(4):290—311, 2000.
11. Fri May 11, 1:30—3:00, Room: GS-F58
    • Lecture 11: Astrée
    • An overview of the Astrée static analyzer.
    • Complements on Astrée from the Programming Language Day at Watson — Hawthorne, on May 7^th, 2007
    • B. Blanchet, P. Cousot, R. Cousot, J. Feret, L. Mauborgne, A. Miné, D. Monniaux, & X. Rival. A Static Analyzer for Large Safety-Critical Software. In PLDI 2003 — ACM SIGPLAN SIGSOFT Conference on Programming Language Design and Implementation, 2003 Federated Computing Research Conference, June 7—14, 2003, San Diego, California, USA, pp. 196—207, ACM Press or any other paper referenced on www.astree.ens.fr.

• Coordinates at IBM
• Course mailing list
• The MIT course 16.399: « Abstract Interpretation » is longer and more detailled. It also provides an extensible abstract interpretor for a mini-languages implementing the concepts presented in this course.