Lecture slides will be posted after each class meeting.
This schedule may change throughout the semester. Check back regularly for updates, including assignment deadlines and other important dates.
| date | topic | slides | notes |
| 8/30/16 | Overview | Read Chapter 1 through 1.5 for Thursday | |
| 9/1/16 | Propositional logic | First homework assigned, due 9/8. | |
| 9/6/16 | Normal forms & satisfiability procedures | We will finish this topic on Thursday | |
| 9/8/16 | Finish DPLL, begin introduction to Dafny | ||
| 9/13/16 | Finish Introduction to Dafny | Second homework assigned, due 9/27. | |
| 9/15/16 | First-order logic | ||
| 9/20/16 | First-order theories | ||
| 9/22/16 | Procedures for FOL with theories (1) | ||
| 9/27/16 | Procedures for FOL with theories (2) | ||
| 9/29/16 | SMT | ||
| 10/4/16 | Program semantics | ||
| 10/6/16 | Proofs using operational semantics | Third homework assigned, due October 25 | |
| 10/11/16 | Specifications & Hoare Logic | ||
| 10/13/16 | Deductive Verification (1) | ||
| 10/18/16 | Deductive Verification (2) | ||
| 10/20/16 | Midterm exam | ||
| 10/25/16 | Termination | ||
| 10/27/16 | Developing inductive annotations (1) | Fourth homework assigned, due November 10 | |
| 11/1/16 | Developing inductive annotations (2) | ||
| 11/3/16 | Strategies for Proving Total Correctness | ||
| 11/8/16 | Intro. to model checking | ||
| 11/10/16 | Temporal Properties | Fifth homework assigned | |
| 11/15/16 | CTL Model Checking | ||
| 11/17/16 | LTL Model Checking | ||
| 11/22/16 | Symbolic model checking | ||
| 11/24/16 | Thanksgiving break | ||
| 11/29/16 | Symbolic Checking, Spin | Sixth homework assigned | |
| 12/1/16 | Model Extraction, Abstraction | ||
| 12/6/16 | Abstraction Refinement | ||
| 12/8/16 | Review | ||
| 12/13/16 | Finals week | ||
| 12/15/16 | Finals week |