Schedule


Lecture notes will be posted after each class until the end of the day.

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


date topic notes asst due asst out live code other
Tue 1/16 Introduction [pdf]
Thu 1/18 Contracts [pdf] HW0 mystery.mlw
Tue 1/23 Data Structures [pdf] mystery.mlw queue.mlw
Thu 1/25 Arrays and Ghosts [pdf] HW0 HW1 intset.mlw bitset.mlw
Tue 1/30 Semantics [pdf]
Thu 2/1 Dynamic Logic [pdf] HW1 HW2
Tue 2/6 Loops [pdf]
Thu 2/8 Arrays [pdf] HW2 HW3 ndl.mlw
Tue 2/13 Induction [pdf] ndl-v2.mlw ind.mlw
Thu 2/15 Diamonds [pdf] HW3 MP1 ndl-v3.mlw
Tue 2/20 Strongest Postconditions [pdf]
Thu 2/22 Sequent Calculus [pdf] MP1 (chkpt)
Tue 2/27 Review I [pdf]
Thu 2/29 Project Day (no lecture) MP1 HW4
Tue 3/5 Spring Break (no classes)
Thu 3/7 Spring Break (no classes)
Tue 3/12 Resolution [pdf]
Thu 3/14 Propositional Encodings [pdf] HW4 HW5 color.py
Tue 3/19 Solving SAT with DPLL [pdf]
Thu 3/21 SMT Theories & Deciding EUF [pdf] HW5 HW6
Tue 3/26 SMT Solving: Nelson-Oppen [pdf]
Thu 3/28 DPLL(T) & SMT Encodings HW6 MP2
Tue 4/2 Bounded Model Checking
Thu 4/4 Linear Temporal Logic MP2 (chkpt)
Tue 4/9 Computation Tree Logic
Thu 4/11 Carnival (no classes)
Tue 4/16 Review II
Thu 4/18 Project Day (no lecture) MP2 HW7
Tue 4/23 Real World Verification
Thu 4/25 Theorem Proving in Lean HW7