Program Analysis

information | timetables | course material | past exam papers

Lecturer	Oege de Moor
Degrees	Part C, Honour School of Computer Science Part C, Honour School of Mathematics and Computer Science Michaelmas Term, MSc in Computer Science MSc by Research
Term	Michaelmas Term 2009 (24 lectures)

overview

Prerequisites Functional programming, plus familiarity with Java. A good understanding of compiler construction is essential. Programming Languages is an advantage but not a necessity.

Program analysis provides the theory, algorithms and engineering techniques to answer questions about your programs. For example, you might want to determine what statements could have contributed to the value of an expression. Another application is for a compiler to decide whether an optimisation can be applied. Or you might want some mechanical assistance when refactoring your program. Program analysis is also indispensable when proving properties of large programs, for instance to check that there are no buffer overflows.

An elegant and crisp mathematical framework is common to all these applications. This course will introduce you to that mathematics, and simultaneously show how it leads to beautiful algorithms that solve practically important problems.

learning outcomes

Students will learn the mathematical theory of lattices, Galois connections, abstract interpretation, and fixpoint computations, Furthermore they will learn to apply those notions in controlflow analysis and dataflow analysis. In turn, those are illustrated by refactoring transformations, optimisations, program understanding tools, and program checkers

synopsis

Overview.
Type-based refactorings: examples and demo.
Definition of extract interface. Type constraints.
Type constraint gathering.
Type constraint solving algorithm.
Introduction to first practical.
Lattice theory: fixpoints.
Computing with fixpoints.
Abstract interpretation and Galois connections.
Abstract interpretation and Galois connections continued.
The Soot framework for analysing Java bytecode.
Small compiler optimisations.
Introduction to second practical.
Call graph construction.
Points-to analysis.
Points-to analysis, continued.
Compiler optimisation: Virtual method call resolution.
Introduction to third practical.
Analysis in program understanding tools.
Slicing
Slicing, continued.
Optimising AspectJ.
Cflow intraprocedural optimisations.
Cflow interprocedural optimisations.

syllabus

Lattice theory: Galois connections; abstract interpretation; fixpoints.
Controlflow analysis and dataflow analysis.
Refactoring transformations: type constraints; solving type constraints.
Range analysis: bounds checking.
Further compiler optimisations: call graph construction; points-to analysis; virtual method resolution.�
Program understanding tools: slicing.

reading list

The main text will be a set of lecture notes. The following are background material:

Flemming Nielson, Hanne Riis Nielson, Chris Hankin: Principles of Program Analysis. Springer (Corrected 2nd printing, 452 pages, ISBN 3-540-65410-0), 2005.
Frank Tip, Adam Kiezun, Dirk Bäumer: Refactoring for generalization using type constraints. OOPSLA 2003: 13-26.
Robert M. Fuhrer, Frank Tip, Adam Kiezun, Julian Dolby, Markus Keller: Efficiently Refactoring Java Applications to Use Generic Libraries. ECOOP 2005: 71-96
Patrick Cousot, Radhia Cousot: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. POPL 1977: 238-252
Ondrej Lhoták, Laurie J. Hendren: Context-Sensitive Points-to Analysis: Is It Worth It?. CC 2006: 47-64
David Grove, Craig Chambers: A framework for call graph construction algorithms. ACM Trans. Program. Lang. Syst. 23(6): 685-746 (2001)
The Soot framework, \verb|http://www.sable.mcgill.ca/soot/|