CMSC 631, Fall 2003

Program Analysis and Understanding


Date Subject Slides Reading Assignment
September 2 Introduction pdf None
September 4 No class
September 9 Dataflow analysis pdf Kildall, A Unified Approach to Global Program Optimization
Kam and Ullman, Global Data Flow Analysis and Iterative Algorithms
(Optional) Aho, Sethi, Ullman, Compilers: Principles, Techniques, and Tools, chapter 10
September 11 pdf Cytron, Ferrante, Rosen, Wegman, and Zadeck, Efficiently Computing Static Single Assignment Form and the Control Dependence Graph
(Optional) Wegman and Zadeck, Constant Propagation with Conditional Branches
hw1, due 9/18
September 16 Tools pdf Evans, Static Detection of Dynamic Memory Errors
Das, Lerner, and Seigle, ESP: Path-Sensitive Program Verification in Polynomial Time
September 18 No class (Hurricane Isabel)
September 23 Abstract Interpretation pdf Jones and Nielson, Abstract Interpretation: a Semantics-Based Tool for Program Analysis (pp1-30 only)
Polyspace, Abstract Interpretation
(Optional) Cousot and Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
September 25 Lambda Calculus
and Functional Programming
pdf (Optional) Introduction to the Objective Caml Programming Language
Also see the O'Caml web page
Also see Bill Pugh's notes on O'Caml
hw2, due 10/2
September 30 Type Systems pdf Cardelli, Type Systems, sections 1-3
October 2 Cardelli, Type Systems, sections 4-6, 9
Damas and Milner, Principle Type-Schemes for Functional Programs
(Optional) Knight, Unification: A Multidisciplinary Survey
hw3, due 10/23
October 7 Guest lecture:
Bill Pugh
Pointer Analysis Ghiya and Hendren, Is it a Tree, a DAG, or a Cyclic Graph? A Shape Analysis for Heap-Directed Pointers in C
Chase, Wegman, and Zadeck, Analysis of pointers and structures
Sagiv, Reps, and Wilhelm, Solving shape-analysis problems in languages with destructive updating
Hind, Pointer Analysis: Haven't We Solved This Problem Yet?
October 9 No class
October 14 Guest Lecture: Mike Hicks
pdf Grossman et al., Region-based Memory Management in Cyclone
Hicks et al, Safe and Flexible Memory Management in Cyclone
October 16 Guest Lecture: Atif Memon None
October 21 Set Constraints pdf Aiken and Wimmers, Type Inclusion Constraints and Type Inference
Heintze and Jaffar, Set-Based Program Analysis
October 23 Axiomatic Semantics pdf,
Rustan's slides
Hoare, An Axiomatic Basis for Computer Programming
Flanagan, Leino, Lillibridge, Nelson, Saxe, and Stata, Extended Static Checking for Java
hw4, due 10/30
October 28 Type Qualifiers pdf Foster, Tachio, and Aiken, Flow-Sensitive Type Qualifiers
October 30 Polymorphic Recursion pdf, ppt Rehof and Fahndrich, Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability

Advice on Giving Research Talks
Peyton Jones, Hughes, and Launchbury, Giving a good research talk
Drysdale, Giving Technical Talks
Hill, Oral Presentation Advice
November 4 Model Checking pdf, ps.gz (1up) more Clarke, Grumberg, and Long, Model Checking (pp1-12 only)
November 6 Student Lectures ppt [Charles]
ppt [George]
Boyapati, Liskov, and Shrira, Ownership Types for Object Enacpsulation [Charles]
Kuncak, Lam, and Rinard, Role Analysis [George]
November 11 ppt [Nick]
ppt [Mujtaba]
Ernst, Cockrell, Griswold, and Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution [Nick]
Hallem, Chelf, Xie, and Engler, A System and Language for Building System-Specific Static Analyses [Mujtaba]
November 12 ppt [Andrey]
pdf [Mike]
Freeman and Pfenning, Refinement Types for ML [Andrey]
Xi and Pfenning, Dependent Types in Practical Programming [Mike]
November 18 ppt [Christian]
ppt [Iulian]
Corbett, Dwyer, Hatcliff, Laubach, Pasareanu, Robby, and Zheng, Bandera: Extracting Finite-State Models from Java Source Code [Christian]
Ball, Rajamani, Automatically Validating Temporal Safety Properties of Interfaces [Iulian]
November 20 pdf [Morgan]
ppt [Nikolaos]
Sagiv, Reps, and Wilhelm, Parametric Shape Analysis via 3-Valued Logic [Morgan]
Moller and Schwartzbach, The Pointer Assertion Logic Engine [Nikolaos]
November 25 pdf [Sandro]
ppt [Brian]
Condit, Harren, McPeak, Necula, and Weimer, CCured in the Real World [Sandro]
Wilson, Uniprocessor Garbage Collection Techniques [Brian]
November 27 No class -- Thanksgiving
December 2 New Directions pdf, ps.gz (1up) None
December 4 Project presentations Christian Almazan and Nick Rutar, A Comparison of Bug Finding Tools for Java
Andrey Utis and Morgan Kleene, Probabilistic Static Branch Prediction via Logic
Charles Lin, Dynamic Refactoring: Steps to a Theory of Validity for Dynamic Software Updates
December 9 Project presentations Brian Krznarich, Safe Support for Region Specific Object Deletion for Cyclone
Mike Furr, Preserving GC Safety and Type Consistency Across Foreign Function Calls
George Caragea and Sandro Fouche, Finite-State Models for Security Systems Validation
December 11 Project presentations Iulian Neamtiu, Finding Semantic Differences Between Programs
Mujtaba Ali, Unique Pointers: Performance, Burden, and Inference
Nikolaos Frangiadakis, Porting to Cyclone using CIL

Valid HTML 4.01!