Schedule

Lecture notes and recordings will be posted after each class meeting.

This schedule is subject to change, so check back regularly for updates.


date topic notes recording asst due asst out live code other
Tue 2/2 Introduction [pdf] [lec01] mystery.c0   mystery.mlw
Thu 2/4 Logical Contracts [pdf] [lec02] fib-init.mlw   fib.mlw   queue.mlw [cap02]
Tue 2/9 Data Structures [pdf] [lec03] Asst 1 [zip] queue.mlw   search.mlw [cap03]
Thu 2/11 Ghosts [pdf]
 [lec04] fibalt.mlw   bset.mlw   regexp.mlw   [cap04]
regexp‑all.mlw   [session]
Tue 2/16 Semantics [pdf] [lec05] Asst 1 Asst 2 [zip] swap.mlw [cap05]
Thu 2/18 Dynamic Logic [pdf] [lec06] [cap06]
Tue 2/23 break day / no class
Thu 2/25 Loops [pdf] [lec07] Asst 2 Asst 3 [zip] [cap07]
Tue 3/2 Arrays [pdf] [lec08] ndl.mlw [cap08]
Thu 3/4 Diamonds [pdf] [lec09] Asst 3 MP 1 [zip] ndl.mlw [cap09]
Tue 3/9 Sequent Calculus [pdf] [lec10] [cap10]
Thu 3/11 Induction [pdf] [lec11] MP 1 / chkpt ind.mlw [cap11]
ndl.mlw   [session]
Tue 3/16 project day / no class
Thu 3/18 SAT Solving [pdf] [lec12] MP 1 [cap12]
midsemester break
Tue 3/23 SAT Encodings [pdf] [lec13] Asst 4 [zip] [cap13]
Thu 3/25 MP1 Review
Tue 3/30 Bounded Model Checking [pdf] [lec15] Asst 4 Asst 5 [zip] cbmc-example.c
sort-bug.c
Thu 4/1 SMT Solving [pdf] [lec16] [cap16]
Tue 4/6 SMT Theories [pdf] [lec17] Asst 5 Asst 6 [zip] [cap17]
Thu 4/8 SMT Encodings [pdf] [lec18] [cap18]
Tue 4/13 SMT Quantifiers [lec19] Asst 6 Asst 7 [zip] [cap19]
Thu 4/15 break day / no class
Tue 4/20 Linear Temporal Logic [lec20] [cap20]
Thu 4/22 LTL Model Checking [lec21] Asst 7 MP 2 [zip] [cap21]
Tue 4/27 Computation Tree Logic [lec22] [cap22]
Thu 4/29 project day / no class
Tue 5/4 Program Synthesis [pdf] [lec23] MP 2 / chkpt
Thu 5/6 MP2 Q&A [lec24]
classes end
Tue 5/11 final exams (in other classes)
Thu 5/13 final exams (in other classes) MP 2