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 asst due asst out live code other
Tue 1/17 Introduction [pdf]
Thu 1/19 Contracts [pdf] HW0 mystery.mlw
Tu 1/24 Data Structures [pdf] mystery.mlw queue.mlw
Thu 1/26 Ghosts [pdf] HW0 HW1 queue.mlw bitset.mlw
Tu 1/31 Semantics [pdf] intset.mlw
Th 2/2 Regular Expressions from Axioms [pdf] HW1 HW2 regexp.mlw
Tu 2/7 Dynamic Logic [pdf]
Th 2/9 Compositional Reasoning [pdf] HW2 HW3
Tu 2/14 Loops [pdf]
Th 2/16 Arrays [pdf] HW3 MP1 ndl.mlw
Tu 2/21 Induction [pdf] ndl.mlw
Th 2/23 Convergence [pdf]
Tu 2/28 Predicate Transformers [pdf]
Th 3/2 Sequent Calculus [pdf]
Tu 3/14 Resolution [pdf]
Th 3/16 Propositional Encodings [pdf] z3_demo.ipynb
Tu 3/21 DPLL [pdf]
Th 3/23 Sound Transformations pureliteral.mlw
Tu 3/28 SMT [pdf]
Th 3/30 Equality and Arrays [pdf]
Tu 4/4 SAT Certificates [pdf]
Th 4/6 Blasting & Quantifiers [pdf]
Tu 4/12 Temporal Logic [pdf]
Th 4/14 Carnival (no classes)
Tu 4/19 Model checking [pdf]
Th 4/21 Linear-time properties [pdf]
Tu 4/24 Checking LTL [pdf]