Lecture notes will be posted after each class meeting. This schedule may change, so check back regularly for updates.

Summary: Cheat Sheet on Dynamic Logic for While Programs

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.