Web Home
Tbpa
Seminar on Type-based Program Analysis
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.
