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. |