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 | 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] | ||||
| Th 3/14 | Resolution | [pdf] | ||||
| Th 3/16 | Propositional Encodings | [pdf] | z3_demo.ipynb | |||
| Th 3/21 | DPLL |