Lecture notes will be posted after each class meeting. This schedule may change, so check back regularly for updates.
| date | topic | notes | comments | |
|---|---|---|---|---|
| 1/14 | Introduction | [pdf] | ||
| 1/16 | Logic & proof |
[pdf] [tex] |
||
| 1/21 | Programs, semantics, & contracts |
[pdf] [tex] |
||
| 1/23 | Contracts & dynamic logic |
[pdf] [tex] |
||
| 1/28 | Compositional reasoning |
[pdf] [tex] |
||
| 1/30 | Invariants for while loops & arbitrary loops |
[pdf] [tex] |
||
| 2/4 | Live coding session, intro to arrays |
[pdf] [tex] |
||
| 2/6 | Arrays & updates |
[pdf] [tex] |
||
| 2/11 | Finish up arrays, total correctness |
[pdf] [tex] |
||
| 2/13 | Loop variants & convergence |
[pdf] [tex] |
||
| 2/18 | More convergence |
[pdf] [tex] |
||
| 2/20 | Data structure invariants |
[pdf] [tex] [mlw] |
mlw Source from live coding exercise | |
| 2/25 | Midterm review | |||
| 2/27 | Midterm exam | |||
| 3/3 | Procedures, contracts, & ghost state |
[pdf] [tex] |
||
| 3/5 | Solving SAT with DPLL |
[pdf] [tex] |
||
| 3/10 | No class, spring break! | |||
| 3/12 | No class, spring break! | |||
| 3/17 | Classes cancelled by university | |||
| 3/19 | SAT Modulo Theories |
[pdf] [tex] |
||
| 3/24 | Real-world SMT |
[pdf] [tex] |
||
| 3/26 | Going temporal & logically so |
[pdf] [tex] |
||
| 3/31 | ω-Automata & computation structures |
[pdf] [tex] |
||
| 4/2 | LTL model checking |
[pdf] [tex] |
||
| 4/7 | Lab 4 Overview & optimized SAT techniques |
[pdf] [tex] |
||
| 4/9 | Emptiness checking ω-Automata |
[pdf] [tex] |
||
| 4/14 | Branching-time properties |
[pdf] [tex] |
||
| 4/16 | No class | |||
| 4/21 | CTL model checking |
[pdf] [tex] |
||
| 4/23 | Abstraction and refinement |
[pdf] [tex] |
||
| 4/28 | CEGAR & Craig Interpolants |
[pdf] [tex] |
||
| 4/30 | Final exam review |