Course Schedule

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