| Date | Subject | Slides | Reading | Assignment |
|---|---|---|---|---|
| September 2 | Introduction | None | ||
| September 4 | No class | |||
| September 9 | Dataflow analysis |
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 |
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 |
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 |
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 | (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 | 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 Cyclone | 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 |
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 | 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 | ||