WSSA'03: David Schmidt's lectures International Winter School on Semantics and Applications
Montevideo, Uruguay, 21-31 July 2003

Abstract interpretation and static analysis

Presented by David Schmidt, Kansas State University

Course description:

A static analysis finitely analyzes a program in advance of the program's execution and extracts information useful for program transformation or program-correctness proofs. Abstract interpretation is a foundational framework that can justify the correctness of a static analysis. Many elegant static analyses are synthesized from the abstract interpretations that justify their correctness.

This series of lectures introduces abstract interpretation and applies it to static analysis. Standard formats of static analysis are presented, and abstract interpretations are used to synthesize both abstract-operational- and abstract-denotational-semantics definitions and as well as logics and models for temporal-logic model checking.

Lecture Materials:

  1. Introduction to abstraction and static analysis (27 May 2004): PS | PS (4 on 1) | PDF
  2. Foundations of abstract interpretation (8 February 2005): PS | PS (4 on 1) | PDF
  3. Mechanics of static analysis (6 July 2004): PS | PS (4 on 1) | PDF
  4. Applications and logics for static analysis (6 July 2004): PS | PS (4 on 1) | PDF

References for further reading are attached to the end of each lecture.

Exam for Course

(Answer any three of the four questions on the exam.)

Last updated 8 February 2005 schmidt at