CS 842 - Static Program Analysis (Fall 2007)

Course Description

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 analysis.

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.

General Information

Organizational meeting:: Thursday, Sept. 13, 2007, 13:00, MC 2036
Class meetings:: Thursdays 13:00 to 16:00, MC 2036
Web page:: http://plg.uwaterloo.ca/~olhotak/cs842
Instructor:: Ondřej Lhoták, olhotak@plg, DC 2520
Office hours:: by appointment

Evaluation

Paper presentations:	25%
Participation in discussions:	15%
Paper summaries:	10%
Course Project:
- proposal:	10%
- final report:	25%
- presentation:	15%

Recommended Reference

Nielson, F., Nielson, H. R., Hankin, C., Principles of Program Analysis, Springer, 2005. (on 24-hour reserve in DC library, circulation desk)

Schedule:

A password-protected local cache of all the readings is here.

Date	(Presenter/Discussant) Papers
Sept. 13	Organizational meeting
Sept. 20	Monotone Dataflow Analysis and Abstract Interpretation (Steve/Alan) John B. Kam and Jeffrey D. Ullman. Monotone Data Flow Analysis Frameworks. Acta Inf., 7:305-317, 1977. (Cameron/Nomair) (2) Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis, 2005, chapter 4 (Abstract Interpretation)
Sept. 27	Type Constraints for Refactoring (no presentation) Frank Tip, Adam Kiezun, and Dirk Baumer. Refactoring for generalization using type constraints. OOPSLA 2003, pages 13-26. (Steve/Zhi) 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. (Zhi/Nomair) Adam Kiezun, Michael D. Ernst, Frank Tip, and Robert M. Fuhrer. Refactoring for Parameterizing Java Classes. ICSE 2007, pages 437-446.
Oct. 4	Points-to Analysis and Call Graph Construction (Cameron/Zhi) O. Shivers. Control flow analysis in Scheme. PLDI 1988, pages 164-174. (Nomair/Cameron) Frank Tip and Jens Palsberg. Scalable propagation-based call graph construction algorithms. OOPSLA 2000, pages 281-293. (no presentation) Ondrej Lhoták and Laurie Hendren. Scaling Java Points-to Analysis Using Spark. CC 2003, pages 153-169.
Oct. 10 (Wednesday) in DC 2314	Context Sensitivity I (Nomair/Zhi) (2) Micha Sharir and Amir Pnueli. Two approaches to interprocedural data flow analysis. In Steven S Muchnick and Neil D Jones, Program Flow Analysis: Theory and Applications, chapter 7, pages 189-233. 1981. (Cameron/Nomair) Ana Milanova, Atanas Rountev, and Barbara G. Ryder. Parameterized object sensitivity for points-to and side-effect analyses for Java. ISSTA 2002, pages 1-11.
Oct. 18	Miscellaneous (Thiago/Jun) Seth Hallem, Benjamin Chelf, Yichen Xie, and Dawson Engler. A system and language for building system-specific, static analyses. PLDI 2002, pages 69-82. (Steve/Thiago) Yichen Xie and Alex Aiken. Scalable error detection using boolean satisfiability. POPL 2005, pages 351-363. (Jun/Steve) 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.
Oct. 25	no class
Nov. 1	Context Sensitivity II (Zhi/Steve) Manu Sridharan and Rastislav Bodík. Refinement-based context-sensitive points-to analysis for Java. PLDI 2006, pages 387-400. (Steve/Cameron) (2) Mooly Sagiv, Thomas Reps, and Susan Horwitz. Precise interprocedural dataflow analysis with applications to constant propagation. Theoretical Computer Science, 167(1-2):131-170, 1996.
Nov. 8	Shape Analysis (Zhi/Steve) (2) Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Solving shape-analysis problems in languages with destructive updating. ACM Transactions on Programming Languages and Systems, 20(1):1-50, January 1998. (no presentation) Mooly Sagiv, Thomas Reps, and Reinhard Wilhelm. Parametric shape analysis via 3-valued logic. POPL 1999, pages 105-118.
Nov. 15	Lightweight Shape Analysis (Zhi/Cameron) Brian Hackett and Radu Rugina. Region-based shape analysis with tracked locations. POPL 2005, pages 310-323. (Cameron/Nomair) Sigmund Cherem and Radu Rugina. Compile-time deallocation of individual objects. ISMM 2006, pages 138-149. (Nomair/Zhi) Stephen Fink, Eran Yahav, Nurit Dor, G. Ramalingam, and Emmanuel Geay. Effective typestate verification in the presence of aliasing. ISSTA 2006, pages 133-144.
Nov. 22	Predicate Abstraction and Path-Sensitive Verification (Alan/Cameron) Thomas Ball, Rupak Majumdar, Todd Millstein, and Sriram K. Rajamani. Automatic predicate abstraction of C programs. PLDI 2001, pages 203-213. (Nomair/Steve) Cormac Flanagan and Shaz Qadeer. Predicate abstraction for software verification. POPL 2002, pages 191-202. (no presentation) Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: path-sensitive program verification in polynomial time. PLDI 2002, pages 57-68.
Nov. 29	Project presentations

Class Discussions

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.

Course Project

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:

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).

For both kinds of project, you will also be required to give an oral presentation to the class.

By October 18th, 2007, submit a project proposal of no more than 4 pages. For a research 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?)

For a survey project, the proposal should address the following:

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 Proceedings format.

Project presentations will take place in class on Thursday, November 29th. Final project reports reports are due one week later, on Thursday, December 6th.