| Date | Subject | Slides | Reading | Assignment |
|---|---|---|---|---|
| August 31 | Introduction | None | ||
| September 2 | Dataflow analysis | Kildall, A Unified Approach to Global Program Optimization | p1 | |
| September 7 | None | h1 | ||
| September 9 | Cytron, Ferrante, Rosen, Wegman, and Zadeck, Efficiently Computing Static Single Assignment Form and the Control Dependence Graph | |||
| September 14 | Abstract Interpretation | Jones and Nielson, Abstract
Interpretation: a Semantics-Based Tool for Program Analysis
(pp1-30 only) (Optional) Cousot and Cousot, Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints | h2 | |
| September 16 | O'Caml | txt | Optional: Developing applications with Objective Caml | |
| September 21 | Lambda Calculus | Pierce, Chapter 5 (Handout) | h3, p2 | |
| September 23 | Type Systems | Cardelli, Type Systems, sections 1-3 | ||
| September 28 | None | h4 | ||
| September 30 | Damas and Milner, Principle Type-Schemes for Functional Programs | p3 | ||
| October 5 | None | h5 | ||
| October 7 | Foster, Johnson, Kodumal, and Aiken, Flow-Insensitive Type Qualifiers (accessible from umd.edu only) | |||
| October 12 | Rehof and Fahndrich, Type-Based Flow Analysis: From Polymorphic Subtyping to CFL-Reachability | h6 | ||
| October 14 | Guest Lecture: Mike Hicks | Jim et al, Cyclone: A Safe Dialect of C | ||
| October 19 | Aiken and Wimmers, Type Inclusion Constraints and Type Inference | |||
| October 21 | Theorem Proving | Hoare, An Axiomatic Basis for Computer Programming | p4 Project proposals due | |
| October 26 | None | |||
| October 28 | ppt examples | Huth and Ryan, chapter 4 (Handout) | ||
| November 2 | Guest Lecture: Bill Pugh | Flanagan and Freund, Type-Based Race Detection for Java | Election day! | |
| November 4 | Guest Lecture: Mike Hicks | ps | Smith, Walker, and Morrisett, Alias Types | |
| November 9 | Guest Lectures Tevfik Bultan, Model Checking | None | ||
| November 11 | Huth and Ryan, Chapter 3 (Handout) Lecture notes (see chapter 5 especially) | |||
| November 16 | Recent Results and Tools | Giving a Good Research Talk ESP: Program Verification of Millions of Lines of Code | ||
| November 18 | The SLAM Project: Debugging System Software via Static Analysis | |||
| November 23 | New Directions | |||
| November 25 | No class -- Thanksgiving | |||
| November 30 | Project Presenations |
Gupta and Srivastava, Dynamic Checking of Dangling Pointer References Jackson, Static Analysis of Perl Speyer, Partially Automated Refactoring Strecker, Inferring Developer Activities by Analyzing Successive Versions of Source Code Weiss and Kobyakov, Design-By-Contract Annotation Set and Runtime Verification for .NET Languages | ||
| December 2 |
Fraser, Automatic Discovery of Integrity Constraints in Binary
Kernel Modules Tran, A Survey on Program Slicing Clancy and McCann, Dynamically Inferring Static Lockset Annotations in C Farrell, Subjective Feedback for Introductory Programmers Sayeed, Abstract Interpretation and Set Constraints in the Type Analysis of Logic Programs | |||
| December 7 |
Arras, Aspect Oriented Programming Zhao and Ma, Inferring Uniqueness of Factory Methods in Java Byrd, Integer Overflow Detection Using Integer Range Analysis Lin, Web Ontology Language Reasoning Blank, A Survey on Efforts toward Completely Automated Program Verification | |||
| December 9 |
Chen and Nakamura, Using Ownership Types to Check Proxy Design
Pattern Use Lumezanu and Udrea, Rule-Based Model Checking of Network Protocols Omatick, Application of Theorem Proving to Programs for Numerical Analysis Halaschek-Wiener and Kolovski, Visualization of CFL-Reachability Graphs | |||