Lecture notes will be posted after each class meeting. This schedule may change, so check back regularly for updates.
| date | topic | notes | comments |
|---|---|---|---|
| 8/29 | Introduction | [pdf] | |
| 8/31 | Propositional logic & proofs | [pdf] | |
| 9/5 | Programs & contracts | [pdf] | |
| 9/7 | Sequential programs & compositional reasoning | [pdf] | |
| 9/7 | Homework 1 due | ||
| 9/12 | Invariants for while loops & arbitrary loops | [pdf] | |
| 9/14 | Live coding session: Introducing Why3 | ||
| 9/14 | Homework 2 due | ||
| 9/19 | Programs with arrays | [pdf] | |
| 9/21 | Better arrays, with updates | [pdf] | |
| 9/21 | Homework 3 due | ||
| 9/26 | Better arrays, with updates (cont'd) | ||
| 9/28 | Diamonds & total correctness | [pdf] | |
| 10/3 | Loop variants & convergence | [pdf] | |
| 10/5 | Solving SAT with DPLL |
[pdf] | |
| 10/5 | Homework 4 due | ||
| 10/5 | Lab 1 due | ||
| 10/10 | Procedures, contracts | [pdf] | |
| 10/12 | Midterm review | ||
| 10/12 | Homework 5 due | ||
| 10/17 | Midterm exam | [solutions] | |
| 10/19 | Recursive procedure calls | [pdf] | |
| 10/24 | Ghost state | [pdf] | |
| 10/26 | Live coding session | ||
| 10/26 | Lab 3 due | ||
| 10/31 | Data structures & invariants | [pdf] | |
| 11/2 | Going temporal & logically so | [pdf] | |
| 11/7 | Computations & Computation Tree Logic | [pdf] | |
| 11/9 | CTL model checking (finishing previous lecture) & dynamic temporal | ||
| 11/14 | LTL model checking | [pdf] | |
| 11/14 | Lab 4 due | ||
| 11/16 | LTL Buchi automata, emptiness checking | [pdf] | |
| 11/21 | No class | ||
| 11/23 | No class | ||
| 11/28 | Software model checking | [pdf] | |
| 11/30 | Abstraction and refinement | [pdf] | |
| 12/5 | CEGAR | [pdf] | |
| 12/8 | Lab 5 due | ||
| 12/7 | Final review | ||
| 12/7 | Final exams begin | Exam date TBD |