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/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
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 Symbolic model checking, part 2
11/30 Existential abstraction
12/5 Abstraction refinement
12/5 Lab 5 due
12/7 Final review
12/7 Final exams begin Exam date TBD