Winter School on Abstract Interpretation

2-6 February 2015

5663896d010df.JPG

Instructor: Jan Midtgaard, Technical University of Denmark, Copenhagen.

Synopsis

The course provides a basic knowledge about abstract interpretation. In the classical framework, the execution of programs is modeled by a transition system. The space of possible executions (the collecting semantics) is then systematically over-approximated through Galois connections. We will study both the theoretical, mathematical foundation, as well as implement the resulting analyses in practice as executable abstract interpreters.

After the course, the participants will have insight into abstract interpretation, the basic theory of approximation (as found in data-flow analysis, program verification, type systems, etc.). The working method of the course will also train the participants to read and understand research papers. At the end of the course, the participants will be able to:

  • describe and explain basic analyses in terms of classic abstract interpretation,
  • apply and reason about Galois connections, and
  • implement abstract interpreters based on the developed program analyses.

The course provides a basic knowledge about abstract interpretation. In the classical framework the execution of programs is modeled by a transition system. The space of possible executions (the collecting semantics) is then systematically over-approximated through Galois connections. We will study both the theoretical, mathematical foundation, as well as implement the resulting analyses in practice as executable abstract interpreters.

The participants will after the course have insight into abstract interpretation, the basic theory of approximation (as found in data-flow analysis, program verification, type systems, etc.). The working method of the course will also train the participants to read and understand research papers. At the end of the course the participants will be able to

  1. describe and explain basic analyses in terms of classic abstract interpretation,
  2. apply and reason about Galois connections, and
  3. implement abstract interpreters based on the developed program analyses.

Resources