CS 842 - Static Program Analysis (Fall 2007)
A static program analysis aims to prove properties about the runtime
behaviour of a program without actually running it. Since interesting
properties are undecidable in general, static analyses provide only an
approximation. A pervasive issue in the design of static analyses is
the trade-off between precision (i.e. the number of programs satisfying
a property for which the property can be proven) and the cost of the
Static analysis was originally motivated by the needs of optimizing
compilers, which transform programs in ways that preserve their
behaviour. Compilation continues to be an important application area
for static analysis. Increasingly, static analysis is also applied in
software development tools, such as program understanding tools, refactoring
tools, and testing and verification tools.
This course covers both fundamental concepts and recent research in
program analysis through in-class discussions of key publications
in the area. While the in-class portion of the course focuses on
program analyses themselves, the project portion is more flexible, and
interested students are encouraged to explore applications of program
analysis in their projects.
- Organizational meeting:
- Thursday, Sept. 13, 2007, 13:00, MC 2036
- Class meetings:
- Thursdays 13:00 to 16:00, MC 2036
- Web page:
- Ondřej Lhoták, olhotak@plg, DC 2520
- Office hours:
- by appointment
|Paper presentations: ||25% |
|Participation in discussions: ||15% |
|Paper summaries: ||10% |
|Course Project: || |
|- proposal: ||10% |
|- final report: ||25% |
|- presentation: ||15% |
- Nielson, F., Nielson, H. R., Hankin, C., Principles of Program Analysis, Springer, 2005. (on 24-hour reserve in DC library, circulation desk)
A password-protected local cache of all the readings is here.
||Monotone Dataflow Analysis and Abstract Interpretation
John B. Kam and Jeffrey D. Ullman.
Monotone Data Flow Analysis Frameworks.
Acta Inf., 7:305-317, 1977.
(2) Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis, 2005,
chapter 4 (Abstract Interpretation)
||Type Constraints for Refactoring
Frank Tip, Adam Kiezun, and Dirk Baumer.
Refactoring for generalization using type constraints.
OOPSLA 2003, pages 13-26.
Robert M. Fuhrer, Frank Tip, Adam Kiezun, Julian Dolby, and Markus Keller.
Efficiently Refactoring Java Applications to Use Generic Libraries.
ECOOP 2005, pages 71-96.
Adam Kiezun, Michael D. Ernst, Frank Tip, and Robert M. Fuhrer.
Refactoring for Parameterizing Java Classes.
ICSE 2007, pages 437-446.
||Points-to Analysis and Call Graph Construction
in DC 2314
|Context Sensitivity I
Seth Hallem, Benjamin Chelf, Yichen Xie, and Dawson Engler.
A system and language for building system-specific, static analyses.
PLDI 2002, pages 69-82.
Yichen Xie and Alex Aiken.
Scalable error detection using boolean satisfiability.
POPL 2005, pages 351-363.
Bruno Blanchet, Patrick Cousot, Radhia Cousot, Jérome Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival.
A static analyzer for large safety-critical software.
PLDI 2003, pages 196-207.
||Context Sensitivity II
||Lightweight Shape Analysis
||Predicate Abstraction and Path-Sensitive Verification
Each student is responsible for thoroughly reading and understanding
each paper that we will be discussing. You may find it helpful for your
understanding to consult other sources.
For each paper, one student will be chosen ahead of time as the presenter.
The presenter will give a 20 to 25-minute presentation explaining the key
contributions of the paper. Another student will be chosen ahead of
time as the discussant. The discussant will have up to 10 minutes to
present limitations of the paper. For a theoretical paper, the discussant
may also identify concepts that are particularly difficult or unclear.
After the discussant, the class as
a whole will discuss the paper, and attempt to clarify any points that
are not clear to everyone.
For papers for which you are neither the presenter nor the discussant,
you will prepare a one-page critique. This is to ensure that everyone
has read and understood all of the papers being discussed. The critique
should include a summary of the paper, as well as your own evaluation
of the contributions and limitations of the paper.
Some of the papers are longer than others. Long papers are marked in
the schedule with a (2). One long paper counts as two short ones:
the presentation of a long paper will be 40 to 50 minutes, the discussant
may have up to 20 minutes, and the critique should be two pages.
The topic of the course project is quite open, but should be related to
program analysis in some way. Feel free to discuss your ideas for project
topics with the instructor.
There are two options for the project:
For both kinds of project, you will also be required to give an
oral presentation to the class.
- Research Project: A research project may involve theoretical
development (i.e. design of an analysis with theorems and proofs
of its properties), implementation, or empirical evaluation, or some
combination of these three. A research project should result in
a written report (maximum 10 pages), a copy of any software implemented,
and any empirical data collected.
- Survey Project: A survey project requires reading additional
publications about a topic, and summarizing and explaining them in a
coherent and organized way. A survey project should result in
a written report (maximum 20 pages).
By October 18th, 2007, submit a project proposal of no more than 4 pages.
For a research project, the proposal should
address the following:
For a survey project, the proposal should address the following:
- Motivation (why is this interesting?)
- Related Work (what has already been done? include references to specific papers)
- Specific Proposal (what exactly do you plan to do, and how will you do it?)
- Expected Results (what do you hope your project will show?)
- Motivation (why is this interesting?)
- Areas of Related Work (give broad categories of related work, and delimit the scope of your survey)
Project reports should submitted as PDF files formatted using the ACM
Project presentations will take place in class on Thursday, November 29th.
Final project reports reports are due one week later, on Thursday, December 6th.