Lectures‎ > ‎

Abstract Interpretation

Speaker: Patrick Cousot


  1. Semantics: We define the structural rule-based and then fixpoint prefix trace semantics of a simple subset of C. We define properties, in particular program properties and collecting semantics.

  2. Abstraction: We formalize the abstraction and approximation of program properties and how a structural rule-based/fixpoint abstract semantics can be derived from the collecting semantics by calculational design.

  3. Proofs: we show that verification methods and program logics are (non-computable) abstractions of the program collecting semantics.

  4. Numerical abstractions: we introduce a few classical effectively computable abstractions of numerical properties of programs and discuss industrial static analysis applications.

  5. Symbolic abstractions: we introduce a few abstractions of symbolic properties of programs and discuss opened problems. We conclude by a list of formal methods that can be formalized as abstract interpretations.