Lecture notes will be posted after each class meeting. This schedule may change, so check back regularly for updates.
| date | topic | notes | comments | |
|---|---|---|---|---|
| 8/28 | Introduction | [pdf] | ||
| 8/30 | Logic & proof | [pdf] | Homework 1 assigned | |
| 9/4 | Programs & contracts | [pdf] | ||
| 9/6 | Sequential programs & compositional reasoning | [pdf] | Homework 1 due ; Homework 2 assigned | |
| 9/11 | Invariants for while loops & arbitrary loops | [pdf] | ||
| 9/13 | Live coding session: Introducing Why3 | [mlw] | Homework 2 due ; Homework 3 and Lab 0 assigned | |
| 9/18 | Programs with arrays | [pdf] | ||
| 9/20 | Arrays & updates | [pdf] | Homework 3 (9/20) and Lab 0 (9/21) due ; Homework 4 assigned | |
| 9/25 | Total correctness | [pdf] | Lab 1 assigned | |
| 9/27 | Loop variants & convergence | [pdf] | Homework 4 due (9/28) | |
| 10/2 | Procedures & contracts | [pdf] | ||
| 10/4 | Parameters & ghost state |
[pdf] | Homework 5 due (10/7) | |
| 10/9 | Midterm review | Lab 1 due | ||
| 10/11 | Midterm exam | |||
| 10/16 | Data structures, invariants, & ghost state | [pdf] | ||
| 10/18 | Solving SAT with DPLL | [pdf] | Lab 2 assigned | |
| 10/23 | Live coding session: Review of Lab1 & Data structures | [mlw] | Introduction to Verified SAT Solver Competition [slides] | |
| 10/25 | SAT Modulo Theories | [pdf] | ||
| 10/30 | Real-world SMT | [pdf] | ||
| 11/1 | Going temporal & logically so | [pdf] | Lab 2 due ; Lab 3 assigned (11/2) | |
| 11/6 | Computations & Computation Tree Logic | [pdf] | ||
| 11/8 | CTL model checking | [pdf] | ||
| 11/13 | Linear-time properties | [pdf] | Lab 3 due ; Lab 4 assigned | |
| 11/15 | Lab 4 Review & Simplifications techniques for SAT | [pdf] | ||
| 11/20 | No class | |||
| 11/22 | No class | |||
| 11/27 | ω-Automata | [pdf] | Lab 4 part 1 due | |
| 11/29 | Software model checking | Homework 6 due (12/2) | ||
| 12/4 | Abstraction and refinement | Lab 4 final due | ||
| 12/6 | Final review | Verified SAT Competition. Additional practice problems available here. |
||
| 12/10 | Final exam | 05:30 p.m. - 08:30 p.m. GHC 4215. |