Static program analysis aims at determining properties about the run-time behaviour of programs without actually executing the program. These properties are then typically used to either verify or optimise the program under analysis.

Over the years, several methodologies for static program analysis have been developed. These include data-flow analysis, constraint-based approaches, and abstract interpretation. In this seminar, we focus on so-called type-based analyses.

A type-based program analysis equips the programming language at hand with a nonstandard type system that stores the properties of interest in the types assignable to programs. An apparent advantage of the type-based approach is that we can reuse to a large extent the tools and techniques developed for ordinary type systems. Examples include polymorphism, subtyping, and type-inference algorithms.

Within the seminar, we will read about and review the state of the art in type-based program analysis. A recurring theme in our exploration will be the intrinsic tension between accuracy and modularity, and the various ways to deal with this tension.

Research papers (available on line).

Introductory lectures, group discussions, presentations by participants.

Paper presentation (30%), mini-project (50%), participation (20%).