| Lec # | topics | key dates |
|---|---|---|
| 1 | Introduction Static and Dynamic Analysis | Assignment 1 out |
| Abstract Interpretation | ||
| 2 | A Semantics-based Tool for Program Analysis | Assignment 1 due |
| 3 | A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints | |
| Dynamic Analysis | ||
| 4 | Chaining Approach for Software Test Data Generation | |
| 5 | Efficient Path Profiling | |
| 6 | Simplifying and Isolating Failure-inducing Input | |
| 7 | Dynamically Discovering Likely Program Invariants to Support Program Evolution | |
| Types | ||
| 8 | Principal Type-schemes for Functional Programs Proofs about a Folklore Let-polymorphic Type Inference Algorithm | |
| 9 | Introduction to Part II, Polymorphic Lambda Calculus | |
| 10 | Lackwit: A Program Understanding Tool based on Type Inference Finding User/Kernel Pointer Bugs with Type Inference | |
| 11 | Points-to Analysis In Almost Linear Time By Type Inference of Programs with Structures and Unions | |
| Model Checking | ||
| 12 | The Spin Model Checker | |
| 13 | Optimizing Symbolic Model Checking for Statecharts | |
| 14 | Constructing Compact Models of Concurrent Java® Programs Using Predicate Abstraction to Reduce Object-oriented Programs for Model Checking | |
| 15-17 | Student Project Presentations | |