8th Estonian Winter School in Computer Science (EWSCS)
VIII Eesti Arvutiteaduse Talvekool (EATTK)
Palmse, Estonia
March 2 - 7, 2003
Patrick Cousot
Département d'Informatique (DI)
École Normale Supérieure (ENS), France
An Introduction to Abstract Interpretation
The objective of the course is to present the formal bases of Abstract Interpretation theory in simple terms and to discuss various applications in Computer Science.
See also http://www.di.ens.fr/~cousot/summerschools/EWSCS03-P-Cousot-course/index.shtml
Content
Lesson 1: Motivations for formal methods;
On formal methods and computer-aided verification;
Motivations for Abstract Interpretation;
Informal introduction to Abstract Interpretation (using a graphical language);
Basic elements of the theory of abstract interpretation: Galois connections, function abstraction, fixpoints, fixpoint approximation and exact abstraction, soundness, completeness.Lesson 2: Elements of Abstract Interpretation (cont'd):
Moore families, closure operators, complements on Galois connections, abstract domains, combination of abtract domains, iterative fixpoint approximation with convergence acceleration by widening/narrowing, completion of abstract domains, the lattice of Abstract Interpretations;
An introductory application to the constructive design of algorithms for grammar analysis;
Application to program verification by predicate abstraction.Lesson 3: Application of Abstract Interpretation to static program analysis;
Formal design of an abstract interpretor.
Course materials
The following two introductory papers are recommended as a written pedagogical support for this course:
- P. Cousot. Semantic foundations of program analysis. In S.S. Muchnick and N.D. Jones, eds, Program Flow Analysis: Theory and Applications, ch 10, pp. 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, ed., Informatics — 10 Years Back, 10 Years Ahead, volume 2000 of Lecture Notes in Computer Science, pp. 138-156. Springer-Verlag, Berlin, 2000.
The last lesson is based on the following paper:
- P. Cousot. The Calculational Design of a Generic Abstract Interpreter. In M. Broy, and R. Steinbrüggen, eds., Calculational System Design, NATO ASI Series F. IOS Press, Amsterdam, 1999.