| Date | Lecture | Readings | Homework,Project |
| Mon 1/3 | Introduction & Type Inference | [DM82],[OJ97] | |
| Wed 1/5 | Type Qualifiers: Format String Bugs,User/Kernel Pointer Bugs | [STFW01], [JW04] | |
| Mon 1/10 | Linear Constraints: Buffer Overrun Detection | [WFBA00], [GCMRJ03] | |
| Wed 1/12 | Concurrency: Types for Races & Atomicity | [FF00], [FQ03] | |
| Mon 1/17 | MLK Day | ||
| Wed 1/19 | Dataflow Analysis, Checking Memory Errors | [K73], [E96] | |
| Mon 1/24 | Abstract Interpretation | [CC77], [BCC+02] | |
| Wed 1/26 | Context-Free Reachability, Summaries: Race,Deadlock Detection | [RHS95], [BR01a], [EA03] | |
| Mon 1/31 | contd. | ||
| Wed 2/2 | Verification Conditions: Extended Static Checking | [F67], [FLL02], [DRS03] | |
| Mon 2/7 | Decision Procedures | [N80] | |
| Wed 2/9 | Proof-Carrying Code, Prefix | [NL96], [BPS00] | |
| Mon 2/14 | Explicit Model Checking, File System Errors | [G97], [YTEM04] | Project proposals Due |
| Wed 2/16 | Presidents' Day | ||
| Mon 2/21 | Symbolic Model Checking | [B86],[BCM+90] | |
| Wed 2/23 | Predicate Abstraction | [GS97] | |
| Mon 2/28 | Counterexample-guided Abstraction Refinement | [BR01b], [HJMS02] | |
| Wed 3/2 | Project Presentations | ||
| Mon 3/7 | Project Presentations | ||
| Wed 3/9 | Project Presentations | Projects Due |