CS 252r: Advanced Topics in Programming Languages

Course description

This course focuses on program analysis, and will survey program analysis concepts, techniques, scalable implementations, and applications. Topics covered are subject to change, but are likely to intersect with the following.

• Dataflow analysis
• Abstract interpretation
• Symbolic execution
• Pointer, alias, and shape analysis
• Control-flow analysis
• Interprocedural analysis
• Model checking
• Dynamic analysis
• Efficient data structures and program representations for analysis

The course will be a combination of lectures and paper discussion. For those taking the course for credit, evaluation will be based on class participation, and a final project. Auditors are welcome.

The course is intended for graduate students at all levels as well as advanced undergraduates. It is expected that students have taken a course in the foundations of programming languages, such as CS 152.

Useful texts

The following texts may be useful as reference or to give additional information on some of the topics covered in class. (Additional texts may be added as the class progresses.)

• Principles of Program Analysis, by Nielson, Nielson, and Hankin. Springer 2005. (Referred to below as NNH.)
• Advanced Compiler Design and Implementation, by Muchnick. Morgan Kaufmann 1997. (Referred to below as Muchnick.)

Schedule

Note 1: Schedule is subject to change. Readings marked "reqd." are required; other readings are optional, and duplicate and/or extend the material discussed in class.

Note 2: Some brief notes on how to read a research paper are available here.

Date	Lec.	Topic	Readings	Slides
Tu 25-Jan	1	Intro Data flow analysis	NNH Chapter 2.1–2.4. Muchnick Chapter 8.
Th 27-Jan	2	Data flow analysis	Composing Dataflow Analyses and Transformations by Lerner, Grove, and Chambers, POPL 02. (Link via Harvard proxy)	.pdf
Tu 1-Feb	3	Paper discussion	ESP: path-sensitive program verification in polynomial time by Das, Lerner, and Seigle, PLDI 02. (reqd.) (Link via Harvard proxy) Presenter: Andrew
Th 3-Feb	4	Static Single Assignment (SSA) form	Efficiently Computing Static Single Assignment Form and the Control Dependence Graph by Cytron, Ferrante, Rosen, Wegman, and Zadeck, TOPLAS 13(4) 1991. (Link via Harvard proxy) A Simple, Fast Dominance Algorithm by Cooper, Harvey, and Kennedy, Software Practice and Experience, 4 2001.	.pdf
Tu 8-Feb	5	Interprocedural analysis	NNH Chapter 2.5. Program Analysis via Graph Reachability by Reps, Information and Software Technology 40(11-12) 1998	.pdf
Th 10-Feb	No class
Tu 15-Feb	6	Pointer analysis	Pointer Analysis: Haven't We Solved This Problem Yet? by Hind, PASTE 01.	.pdf
Th 17-Feb	7	Paper discussion	Strictly Declarative Specification of Sophisticated Points-to Analyses by Bravenboer and Smaragdakis, OOPSLA 2009. (reqd.) (Link via Harvard proxy) Presenter: Scott Points-To Analysis with Efficient Strong Updates by Lhotak and Chung, POPL 11. (reqd.) (Link via Harvard proxy) Presenter: Dan
Tu 22-Feb	8	Paper discussion	Pick Your Contexts Well: Understanding Object-Sensitivity by Smaragdakis, Bravenboer, and Lhotak, POPL 11 (reqd.) (Link via Harvard proxy) Presenter: Youngjune Scaling CFL-Reachbility-Based Points-To Analysis Using Context-Sensitive Must-Not-Alias Analysis by Xu, Rountev, and Sridharan, ECOOP 2009 (reqd.) No presenter
Th 24-Feb	9	Shape analysis	Parametric shape analysis via 3-valued logic by Sagiv, Reps, and Wilhelm, POPL 99. (Link via Harvard proxy) Region-Based Shape Analysis with Tracked Locations by Hackett and Rugina, POPL 05 (Link via Harvard proxy)	.pdf
Tu 1-Mar	10	Control-flow analysis	NNH Chapter 3. Resolving and exploiting the k-CFA paradox: Illuminating functional vs. object-oriented program analysis by Might, Smaragdakis, and Van Horn, PLDI 2010 (Link via Harvard proxy) Control-flow analysis of functional programs by Midtgaard, ACM Computing Surveys 2010	.pdf
Th 3-Mar	11	Abstract interpretation	NNH Chapter 4. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints by Cousot and Cousot, POPL 1977. Systematic Design of Program Analysis Frameworks by Cousot and Cousot POPL 1979.	.pdf (contains link to the NNH Chap. 4 slides)
Tu 8-Mar	12	Project proposal due Abstract interpretation		.pdf
Th 10-Mar	No class
Spring Recess
Tu 22-Mar	13	Symbolic execution	Symbolic execution and program testing by King, CACM 19(7) 1976 (Link via Harvard proxy) See http://sites.google.com/site/symexbib/ for a bibliography of symbolic execution related papers.	.pdf
Th 24-Mar	14	Paper discussion	KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs by Cadar, Dunbar, and Engler, OSDI 2008 (reqd.) Mixing type checking and symbolic execution by Khoo, Chang, and Foster, PLDI 2010 (reqd.) (Link via Harvard proxy)	.pdf
Tu 29-Mar	15	Paper discussion	The Reachability Bound Problem by Gulwani and Zuleger, PLDI 10. (reqd.) (Link via Harvard proxy)	See Sumit Gulwani's lecture notes from a guest lecture in Jens Palsberg's UCLA program analysis course. .pdf
Th 31-Mar	16	Model checking	Data Flow Analysis is Model Checking of Abstract Interpretations by Schmidt, POPL 98. (Link via Harvard proxy) See 25 Years of Model Checking Symposium (2006) for some interesting retrospectives.	.pdf
Tu 5-Apr	17	Paper discussion	Automatic Predicate Abstraction of C Programs by Ball, Majumdar, Millstein, and Rajamani, PLDI 2001 (reqd.) The SLAM Project: Debugging System Software via Static Analysis by Ball and Rajamani, POPL 2002 (reqd.) (Link via Harvard proxy)
Th 7-Apr	18	Dynamic information	Whole Program Paths by Larus, PLDI 99. (reqd.) (Link via Harvard proxy) The Cooperative Bug Isolation Project. The paper Reflections on the Role of Static Analysis in Cooperative Bug Isolation by Liblit, SAS 2008, provides an overview of the approach, and how other (static) program analyses are used.
Tu 12-Apr	19	Analysis of low-level code	There's plenty of room at the bottom: Analyzing and verifying machine code (Invited tutorial) by Reps, Lim, Thakur, Balakrishnan, and Lal, CAV 10. Native Client: A Sandbox for Portable, Untrusted x86 Native Code by Yee, Sehr, Dardyk, Chen, Muth, Ormandy, Okasaka, Narula, and Fullagar, Oakland 2009. Presenter: Gregory
Th 14-Apr	20	Analysis of dynamic languages	The Essence of JavaScript by Guha, Saftoiu, and Krishnamurthi, ECOOP 2010.
Tu 19-Apr	21	Experimental methodology	Producing Wrong Data Without Doing Anything Obviously Wrong! by Mytkowicz, Diwan, Hauswirth, and Sweeney, ASPLOS 09. (Link via Harvard proxy) Wake up and smell the coffee: evaluation methodology for the 21st century by Blackburn et al., CACM 51(8) 2008. (Link via Harvard proxy)
Th 21-Apr	No class
Tu 26-Apr	22	Project presentations
We 27-Apr		Final project due