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] | |||||
| 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] |