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


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/19 Programs with arrays [pdf]
9/21 Better arrays, with updates
9/26 Diamonds & total correctness
9/28 Ghost in the proof: using auxiliary state
10/3 A look inside the machine: VC generators and decision procedures
10/5 DPLL, with and without theories
10/10 Procedures & contracts
10/10 Lab 2 due
10/12 Midterm review
10/17 Midterm exam
10/19 Lemmas
10/24 More lemmas: proofs as programs
10/26 Memory models & aliasing
10/26 Lab 3 due
10/31 Verifying programs with aliasing, part 1
11/2 Verifying programs with aliasing, part 2
11/7 Introduction to model checking
11/9 Modeling temporal properties with CTL
11/14 CTL model checking
11/14 Lab 4 due
11/16 Temporal correctness
11/21 Symbolic model checking, part 1
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