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 |