16.399: Abstract Interpretation

Spring term 2005

Content:

• Course information
• Instructor
• Course objective and themes
• Course description
• Course notes
• Course schedule
• Assignments
• Personnal project
• Grading
• Final exam problem
• Bibliographic reference

Course number: 16.399
Title: Abstract Interpretation
Units: H level course, 3-0-9
Lecture hours: Tuesday 11:00–12:30 and Thursday 11:00–12:30 (see the course schedule for exceptions)
Location: 33–419
Course web site: http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www
Prerequisites: basic skill in mathematics and experience with computer programming.

Patrick Cousot
Jerome Clarke Hunsaker Visiting Professor at the MIT Aeronautics and Astronautics Department
Professor at the Computer Science Department of the École Normale Supérieure in Paris (France)

Office: 33—219
MIT Aero-Astro
125 Massachusetts Av.
Boston MA 02139 U.S.A.
Tel: 617–253–7439
Email: cousotmitedu

Office hours: after class or by email appointment

Course Objective and Themes:

• The software verification problem: specification, testing (debugging, simulation, code review), verification by formal methods (deductive methods, model-checking, static analysis) and their limitations (undecidability, complexity), intuitive notion of approximation, false alarms);
• Mathematical foundations (naive set theory, first order classical logic, lattice theory, fixpoint theory);
• Semantics of programming languages (abstract syntax, operational semantics, inductive definitions, example of a simple imperative language, grammar and interpretor of the language, trace semantics);
• Program specification and manual proofs (safety properties, Hoare logic, predicate transformers, liveness properties, linear-time temporal logic (LTL));
• Order-theoretic approximation (abstraction, closures, Galois connections, fixpoint abstraction, widening, narrowing, reduced product, absence of best approximation, refinement);
• Principle of static analysis by abstract interpretation (reachability analysis of a transition system, finite approximation, model-checking, infinite approximation, static analysis, program-based versus language-based analysis, limitations of finite approximations);
• Design of a generic structural abstract interpreter (collecting semantics, non-relational and relational analysis, convergence acceleration by widening/narrowing);
• Static analysis (forward reachability analysis, backward analysis, iterated forward/backward analysis, inevitability analysis, termination);
• Numerical abstract domains (intervals, affine equalities, congruences, octagons, polyhedra);
• Symbolic abstract domains (abstraction of sequences, trees and graphs, BDDs, word and tree automata, pointer analysis);
• Case studies (abstractions used in ASTRÉE and TVLA);

Course Notes:

The course slides are available along with the course schedule.

Course Schedule:

• Thursday February 10^th, 2005, Lecture 1: A short informal presentation of the course topic followed by a discussion with the students to adjust the course content to their desiderata. Here are the slides and the corresponding reading assignment.
• Tuesday February 15^th, 2005, Lecture 2: A discussion of the software verification problem, classical program proof methods. Here are the slides and the corresponding reading assignment.
• Thursday February 17^th, 2005, Lecture 3: undecidabily, complexity, automatic abstract termination proofs by semidefinite programming. Here are the slides and the corresponding programs (that require Matlab^® (commercial), YALMIP of Johan Löfberg and the corresponding solvers), examples (in compressed form) and reading assignment.
• Tuesday February 22^nd, 2005: No lecture (Monday schedule of classes to be held).
• Thursday February 24^th, 2005: No lecture (students should learn about Ocaml).
• Tuesday March 1^st, 2005, Lecture 4: Naïve set theory. Here are the slides. The reading assignment explores the Z notation for describing computer-based systems, which is based on Zermelo-Fraenkel set theory and first order predicate logic.
• Thursday March 3^rd, 2005, Lecture 5: Operational semantics. Here are the slides. The reading assignment explores the informal operational semantics of C. The course uses a simple imperative language (SIL, see program examples) for which a parser/pretty printer and a definitional standard interpreter are provided in Ocaml.
• Tuesday March 8^th, 2005, Lecture 6: First order logic. Here are the slides. The reading assignment explores programs as predicates.
• Thursday March 10^th, 2005, Lecture 7: Program properties: semantics, specification, logics. Here are the slides and 3-2 filter program. The reading assignment explores program specification using the synchronous dataflow programming language Lustre.
• Tuesday March 15^st, 2005, Lecture 8: Big-step collecting semantics; Program property classification (safety/liveness). Here are the slides. The reading assignment is on safety/liveness.
• Thursday March 17^th, 2005, Lecture 9: Lattice theory — Part I. Here are the slides. The reading assignment is on static analysis with TDGs (extensions of BDDs)
• Tuesday March 22^nd, 2005 No course, spring vacation.
• Thursday March 24^th, 2005 No course, spring vacation.
• Tuesday March 29^th, 2005, Lecture 10: Lattice theory — Part II Here are the slides. Ordered maps, Closures and Galois connections, part I. Here are the slides. The reading assignment is on logical relations and Galois connections.
• Thursday March 31^st, 2005: No course, NSF panel.
• Tuesday April 5^th, 2005, Lecture 11: Ordered maps, Closures and Galois connections, part II. Here are the slides. Fixpoints, Part I. Here are the slides. The reading assignment is on fixpoint theorems.
• Thursday April 7^th, 2005, Lecture 12: Fixpoints, Part II and inductive definitions. Here are the slides. The reading assignment is on asynchronous iterations with memory, it will allow to give a very short proof of the special case of boolean equations.
• Tuesday April 12^th, 2005, Lecture 13: Abstraction, Part I. Here are the slides and the reading assignment.
• Thursday April 14^th, 2005, Lecture 14: Abstraction, Part II. Here are the slides. Reachability and postcondition semantics. Here are the slides. The reading assignment is on the initial presentation of this material. The reachability and postcondition collecting semantics of SIL is given in the form of a collecting interpretor written in Ocaml.
• Tuesday April 19^th, 2005: No course, Patriots Day—Vacation.
• Thursday April 21^th, 2005, Lecture 15: Approximation. Here are the slides (and the example iteration OCaml program). The reading assignment is on the initial presentation of this material.
• Tuesday April 26^th, 2005, Lecture 16: Non-relational monotonic finitary static analysis, part I. Here are the slides. There is no reading assignment but the personnal project homework assignment 1 is proposed instead.
• Thursday April 28^th, 2005: No course, NSF panel.
• Tuesday May 3^rd, 2005, Lecture 17: Non-relational monotonic finitary static analysis, part II. Here are the slides. There is no reading assignment but the personnal project homework assignment 2 is proposed instead.
• Thursday May 5^th, 2005, Lecture 18: Non-relational, non-monotonic infinitary static analysis by convergence acceleration with widening/narrowing. Here are the slides. The optional reading assignment is on widenings in interprocedural analysis.
• Tuesday May 10^th, 2005, Lecture 19: Iterative reduced product. Linearization. Polyhedral relational static analysis. Here are the slides. The reading assignment and/or the homework assignment 3 are both optional.
• Thursday May 12^th, 2005, Lecture 20, last class: Iterated forward/backward analysis. Short presentation of theASTRÉE static analyser. Here are the slides. The optional reading assignment considers approximations of other combinations of fixpoints, extending the results presented in the course to a subset of the µ-calculus. The homework assignment 4 is also optional.
• Friday May 13^th, 2005, Minta Martin Lecture: 4:00—5:00 pm, in the Bartos Theater (E15-054).
• Tuesday May 16—20^th, 2005: Final exam week
  • Final writen exam on Monday, May 16, room 33-422, from 9:00—12:00.
  • Final oral exam on Monday, May 16, room 33-308 starting 4:00pm

Assignments:

• Reading assignment of Lecture 1, Thursday February 10^th, 2005:
  

  Patrick Cousot. Abstract Interpretation Based Formal Methods and Future Challenges. In Informatics, 10 Years Back — 10 Years Ahead, R. Wilhelm (Ed.), Lecture Notes in Computer Science 2000, Springer, pp. 138–156, 2001.

• Reading assignment of Lecture 2, Tuesday February 15^th, 2005:

  Gerard J. Holzmann. Trends in Software Verification. In Proceedings FME 2003: Formal Methods, International Symposium of Formal Methods Europe, Pisa, Italy, September 88–14, 2003, K. Araki, S. Gnesi and D. Mandrioli (Eds.), Lecture Notes in Computer Science 2805, Springer, pp. 40–50, 2003.

• Reading assignment of Lecture 3, Thursday February 17^th, 2005:

  Patrick Cousot. Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming. In Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI'05), Paris, France, January 17—19, 2005. LNCS 3385, Springer, Berlin, pp. 1—24.

• Reading assignment of Lecture 4, Tuesday March 1^st, 2005:

  J. M. Spivey. The Z Notation: A Reference Manual, 2nd edition, Prentice-Hall, 168 p., 1992. Read Chapter 1, « Tutorial Introduction », pp. 1—23.

• Reading assignment of Lecture 5, Thursday March 3^rd, 2005:

  Study the syntax and semantics of integer type declarations, the evaluation of integer arithmetic expressions, the evaluation of boolean expressions and the execution of assignments, tests and iterations for the C programming language either in the 1975 C Reference Manual by Brian W. Kernighan and Dennis M. Ritchie or in the 1999 standard definition of the C programming language.

• Reading assignment of Lecture 6, Tuesday March 8^th, 2005:

  E.C.R. Hehner: Specifications, Programs, and Total Correctness, Science of Computer Programming, volume 34, pp. 191–205, 1999.

• Reading assignment of Lecture 7, Tuesday March 10^th, 2005:

  N. Halbwachs, P. Caspi, P. Raymond and D. Pilaud. ``The synchronous dataflow programming language Lustre''. Proceedings of the IEEE, vol. 79, nb. 9. September 1991 (to be gunziped to get ps).

• Reading assignment of Lecture 8, Tuesday March 15^th, 2005:

  Fred B. Schneider. ``Decomposing Properties into Safety and Liveness using Predicate Logic. Cornell University Computer Science Department Technical Report TR 87-874, October 1987 (pdf (1)).

• Reading assignment of Lecture 9, Thursday March 17^th, 2005:

  Laurent Mauborgne. ``Abstract Interpretation Using Typed Decision Graphs''. Science of Computer Programming, 31(1):91—112, May 1998.

• Reading assignment of Lecture 10, Tuesday March 28^th, 2005:

  Kevin Backhouse and Roland Backhouse ``Galois Connections and Logical Relations''. Int. Conf. on Mathematics of Program Construction, Dagstuhl, Germany, July 2002. Springer Verlag LNCS 2386, pp. 23—39. Here is a journal version.

• Reading assignment of Lecture 11, Tuesday April 5^th, 2005:

  Federico Echenique A short and constructive proof of Tarski's fixed-point theorem. International Journal of Game Theory, 2005.

• Reading assignment of Lecture 12, Thursday April 7^th, 2005:

  Patrick Cousot. Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice.. In Research Report R.R. 88, Laboratoire IMAG, University of Grenoble, France. 15 pages. September 1977.

• Reading assignment of Lecture 13, Tuesday April 12^th, 2005:

  Patrick Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, editors, Program Flow Analysis: Theory and Applications, Ch. 10, pages 303—342, Prentice-Hall, 1981.

• Reading assignment of Lecture 14, Thursday April 14^th, 2005:

  Patrick Cousot and Radhia Cousot. Systematic Design of Program Analysis Frameworks. In Conference Record of the Sixth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 269—282, San Antonio, Texas, 1979. ACM Press, New York.

• Reading assignment of Lecture 15, Thursday April 21^st, 2005:

  Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the Fourth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 238—252, Los Angeles, California, 1977. ACM Press, New York, NY, USA.

• Reading assignment of Lecture 16, Tuesday April 28^th, 2005:

  None, but the personnal project homework assignement 1 is proposed instead.

• Reading assignment of Lecture 17, Tuesday May 3^rd, 2005:

  None, but the personnal project homework assignement 2 is proposed instead.

• Optional reading assignment of Lecture 18, Thursday May 5^th, 2005:

  François Bourdoncle, Abstract interpretation by dynamic partitioning Journal of Functional Programming, Vol. 2, No. 4 (1992) 407—435.

• Optional reading assignment of Lecture 19, Tuesday May 10^th, 2005:

  Nicolas Halbwachs, About synchronous programming and abstract interpretation. International Symposium on Static Analysis, SAS'94, LNCS 864, Springer Verlag. Namur (Belgium), September 1994.

• Optional reading assignment of Lecture 20, Thursday May 12^th, 2005:

  Damien Massé, Combining Forward and Backward Analyses of Temporal Properties. PADO 2001, O. Danvy, A. Filinski (Eds.), Lecture Notes in Computer Science 2053, pp. 103—116, Springer 2001

Project:

• The personnal project is to be written in OCaml for which compilers are freely available on many platforms. Here are course notes on OCaml as well as corresponding programming examples.

• The personnal project is on the design and implementation of a static analyzer of numerical programs written in SIL (a simple imperative language).
  • The syntax and operational semantics of SIL has been formally specified in lecture 5 and respectively implemented in Ocaml by a parser/pretty printer and a definitional standard interpreter
  • Here are SIL program examples
  • The reachability collecting semantics described in Lecture 15 has been implemented in a collecting interpretor
  • The non-relational initialization and simple sign analysis of SIL described in lecture 16 is provided below:
    • With forward-only analysis of boolean expressions
    In lecture lecture 17, we studied several refinements of non-relational analyses:
    • With forward & backward analysis of boolean expressions
    • With local decreasing iterations for forward & backward analysis of boolean expressions
    • With local decreasing iterations for forward & backward analysis of boolean expressions and assignments

• Homework 1:
  • Change file avalues.ml of the non-relational initialization and simple sign abstract interpretors discussed in Lecture 16 to implement a finitary analysis of your choice (e.g. initialization analysis, Killdall's constant propagation, enriched sign analysis, etc, preferably based on your own ideas).
  • Provide the abstraction and concretization functions for sets of concrete values as comments in the file.
  • The main design criteria should be originality and soundness

• Homework 2:
  • Change file avalues.ml of the non-relational initialization and simple sign abstract interpretors with backward analysis of expressions discussed in Lecture 17 to implement the finitary analysis that you have chosen.

• Homework 3 (optional):
  • Given the generic forward relational analyzer, modify the polyhedral analysis in file aenv.ml to implement an octagonal analysis using the The Octagon Abstract Domain Library (which interface is similar to that of New Polka used in the course), or
  • Modify the polyhedral analysis in file aenv.ml to handle strict inequalities

• Homework 4 (optional):
  • The generic iterative pre/postcondition static analyzer is available online as well as the polyhedral analaysis instance
  • Instanciate the analyzer for octagonal analysis using the The Octagon Abstract Domain Library

Grading:

The course is letter graded.

The grading proposal below is tentative and is to be discussed with the course participants.


	10%	Class participation
	30%	Presentation
	40%	Personal project
	20%	Final writen exam, open book, 3 hours, Monday, May 16 from 9—12, room 33-422

The presentation of a research paper will be in Computer Science conference format (25mn of talk and 5mn of questions). The article is to be selected by the students in the list of assigned readings. Issues about giving a talk are discussed here. The presentations will be held outside of lecture hours during the finals week — on Monday, May 16, room 33-308, starting 4:00pm.

Final exam problem:

• Here is the final exam problem (which consists in proving that model checking is an abstract interpretation of the temporal formulæ semantics)

Bibliographic reference:

   @unpublished{Cousot-MITcourse05,
      author =  {P.~Cousot},
      title =   {Abstract interpretation},
      note =    {MIT course 16.399, \url{http://web.mit.edu/16.399/www/}},
      month =   {Feb.--May},
      year =    2005,
   }