Here is a list of papers that will form the basis for this course. Note that this list is neither sound nor complete: we will not read every paper on the list, and we will read papers that are not on the list. The list is also not in any particular order.

Papers for student presentations

Papers that are already taken list the presenter afterward.

• Boyapati, Liskov, and Shrira, Ownership Types for Object Enacpsulation (or any ownership types paper) [Charles]
• Wilson, Uniprocessor Garbage Collection Techniques [Brian]
• Ernst, Cockrell, Griswold, and Notkin, Dynamically Discovering Likely Program Invariants to Support Program Evolution (or any Daikon paper) [Nick]
• Hallem, Chelf, Xie, and Engler, A System and Language for Building System-Specific Static Analyses (or any meta-level compilation paper) [Mujtaba]
• Sagiv, Reps, and Wilhelm, Parametric Shape Analysis via 3-Valued Logic (or any TVLA paper) [Morgan]
• Freeman and Pfenning, Refinement Types for ML [Andrey]
• Xi and Pfenning, Dependent Types in Practical Programming [Mike]
• Ball, Rajamani, Automatically Validating Temporal Safety Properties of Interfaces [Iulian]
• Moller and Schwartzbach, The Pointer Assertion Logic Engine [Nikolaos]
• Corbett, Dwyer, Hatcliff, Laubach, Pasareanu, Robby, and Zheng, Bandera: Extracting Finite-State Models from Java Source Code [Christian]
• Condit, Harren, McPeak, Necula, and Weimer, CCured in the Real World [Sandro]

Papers not yet scheduled

• Millner, A Theory of Type Polymorphism in Programming
• Holzmann, The Model Checker Spin
• Clarke, Grumberg, and Long, Verification Tools for Finite-State Concurrent Systems
• Reps, Horwitz, and Sagiv, Precise Interprocedural Dataflow Analysis via Graph Reacability
• Strom and Yemini, Typestate: A Programming Language Concept for Enhancing Software Reliability
• Tofte and Talpin, Implementation of the Typed Call-by-Value &lgr;-Calculus Using a Stack of Regions
• Crew, ASTLOG: A Language for Examining Abstract Syntax Trees
• Shankar, Talwar, Foster, and Wagner, Detecting Format-String Vulnerabilities with Type Qualifiers
• DeLine and Fanhdrich, Enforcing High-Level Protocols in Low-Level Software
• Chase, Wegman, and Zadeck, Analysis of Pointers and Structures
• Steensgaard, Points-to Analysis in Almost Linear Time
• Heintze and Tardieu, Ultra-Fast Aliasing using CLA: A Million Lines of C Code in a Second
• Bush, Pincus, and Sielaff, A static analyzer for finding dynamic programming errors
• Fahndrich, Foster, Su, and Aiken, Partial Online Cycle Elimination in Inclusion Constraint Graphs
• Boyer and Moore, Program Verification
• Choi, Lee, Loginov, O'Callahan, Sarkar, and Sridharan, Efficient and Precise Datarace Detection for Multithreaded Object-Oriented Programs
• Savage, Burrows, Nelson, Sobalvarro, and Anderson, Eraser: A Dyanmic Data Race Detector for Multi-Threaded Programs
• Flanagan and Freund, Type-Based Race Detection for Java
• Crary, Walker, and Morrisett, Typed Memory Management in a Calculus of Capabilities
• Guyer and Lin, Client-Driven Pointer Analysis
• Hovemeyer and Pugh, Finding Bugs is Easy
• Igarashi and Kobayashi, Resource Usage Analysis
• Turner, Wadler, and Mossin, Once Upon a Type
• Plotkin, A Structural Approach to Operational Semantics
• Remy, Type Checking Records and Variants in a Natural Extension of ML
• Schmidt, Data Flow Analysis is Model Checking of Abstract Interpretations
• Shivers, Control-Flow Analysis in Scheme
• Henzinger, Jhala, Majumdar, and Sutre, Lazy Abstraction
• Mitchell, Type inference with simple subtypes
• Wadler, Proofs are Programs: 19th Century Logic and 21st Century Computing
• Flanagan, Flatt, Krishnamurthi, Weirich, and Felleisen, Catching Bugs in the Web of Program Invariants
• O'Callahan and Jackson, Lackwit: A Program Understanding Tool Based on Type Inference (see also Ajax)

Papers that have been scheduled

• Kam and Ullman, Global Data Flow Analysis and Iterative Algorithms
• Kildall, A Unified Approach to Global Program Optimization
• Cytron, Ferrante, Rosen, Wegman, and Zadeck, Efficiently Computing Static Single Assignment Form and the Control Dependence Graph
• Wegman and Zadeck, Constant Propagation with Conditional Branches
• Evans, Static Detection of Dynamic Memory Errors
• Das, Lerner, and Seigle, ESP: Path-Sensitive Program Verification in Polynomial Time
• Jones and Nielson, Abstract Interpretation: a Semantics-Based Tool for Program Analysis (pp1-30 only)
• Polyspace, Abstract Interpretation
• Cousot and Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints
• Cousot and Cousot, Systematic Design of Program Analysis Frameworks (not scheduled)
• Cardelli, Type Systems
• Damas and Milner, Principle Type-Schemes for Functional Programs
• Knight, Unification: A Multidisciplinary Survey
• Aiken and Wimmers, Type Inclusion Constraints and Type Inference
• Heintze and Jaffar, Set-Based Program Analysis
• Hoare, An Axiomatic Basis for Computer Programming
• Flanagan, Leino, Lillibridge, Nelson, Saxe, and Stata, Extended Static Checking for Java
• Grossman, Morrisett, Jim, Hicks, Wang, and Cheney, Region-Based Memory Management in Cyclone
• Foster, Tachio, and Aiken, Flow-Sensitive Type Qualifiers
• Rehof and Fahndrich, Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability
• Clarke, Grumberg, and Long, Model Checking