16.399: Abstract Interpretation |
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
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. |
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. |
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. |
J.
M. Spivey. The Z Notation: A Reference Manual, 2^{nd} edition, Prentice-Hall, 168 p., 1992. Read Chapter 1, « Tutorial Introduction », pp. 1—23. |
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. |
E.C.R. Hehner: Specifications, Programs, and Total Correctness, Science of Computer Programming, volume 34, pp. 191–205, 1999. |
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). |
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)}). |
Laurent Mauborgne. ``Abstract Interpretation Using Typed Decision Graphs''. Science of Computer Programming, 31(1):91—112, May 1998. |
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. |
Federico Echenique A short and constructive proof of Tarski's fixed-point theorem. International Journal of Game Theory, 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. |
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. |
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. |
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. |
None, but the personnal project homework assignement 1 is proposed instead. |
None, but the personnal project homework assignement 2 is proposed instead. |
François Bourdoncle, Abstract interpretation by dynamic partitioning Journal of Functional Programming, Vol. 2, No. 4 (1992) 407—435. |
Nicolas Halbwachs, About synchronous programming and abstract interpretation. International Symposium on Static Analysis, SAS'94, LNCS 864, Springer Verlag. Namur (Belgium), September 1994. |
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 |
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 |
@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, }