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 | recording | asst due | asst out | live code | other |
|---|---|---|---|---|---|---|---|
| Tue 1/18 | Introduction | [pdf] | [lec01] | ||||
| Thu 1/20 | Logical Contracts | [pdf] | [lec02] | Asst 0 [zip] | mystery.mlw | [cap02] | |
| Tue 1/25 | Data Structures | [pdf] | [lec03] | mystery.mlw queue.mlw | [cap03] | ||
| Thu 1/27 | Arrays and Ghosts | [pdf] | [lec04]* | Asst 0 | Asst 1 [zip] | intset.mlw bitset.mlw | *w/o rap |
| Tue 2/1 | Semantics | [pdf] | [lec05] | regexp-spec.mlw | |||
| Thu 2/3 | Dynamic Logic | [pdf] | [N/A] | Asst 1 | Asst 2 [zip] | regexp.mlw | |
| Tue 2/8 | Loops | [pdf] | [lec07] | ||||
| Thu 2/10 | Arrays | [pdf] | [lec08] | Asst 2 | Asst 3 [zip] | ndl-v1.mlw | |
| Tue 2/15 | Induction | [pdf] | [lec09] | ind.mlw ndl-live.mlw ndl-v2.mlw | |||
| Thu 2/17 | Convergence | [pdf] | [lec10] | Asst 3 | MP 1 [zip] | ||
| Tue 2/22 | Strongest Postconditions | [pdf] | [lec11] | ndl-v3.mlw | |||
| Thu 2/24 | Sequent Calculus | [pdf] | [lec12] | MP 1 (chkpt) | |||
| Tue 3/1 | Resolution | [pdf] | [lec13] | ||||
| Thu 3/3 | Project Day (no lecture) | MP 1 | Asst 4 [zip] | ||||
| Tue 3/8 | Spring Break (no classes) | ||||||
| Thu 3/10 | Spring Break (no classes) | ||||||
| Tue 3/15 | Solving SAT with DPLL | [pdf] | [lec14] | ||||
| Thu 3/17 | Propositional Encodings | [pdf] | [lec15] | Asst 4 | Asst 5 [zip] | z3_demo.ipynb | |
| Tue 3/22 | Bit-Blasting | [pdf] | [lec16] | ||||
| Thu 3/24 | Bounded Model Checking | [pdf] | [lec17] | Asst 5 | Asst 6 [zip] | bmc_live.ipynb bmc.py | |
| Tue 3/29 | Deciding Arrays and Uninterpreted Functions | [pdf] | [lec18] | ||||
| Thu 3/31 | Satisfiability Modulo Theories | [pdf] | [N/A] | Asst 6 | Asst 7 | ||
| Tue 4/5 | SAT & SMT Certificates | [pdf] | [lec20] | ||||
| Thu 4/7 | Carnival (no classes) | ||||||
| Tue 4/12 | More Certificates | [pdf] | [lec21] | ||||
| Thu 4/14 | Temporal Logic | [pdf] | [lec22] | Asst 7 | MP 2 | ||
| Tue 4/19 | CTL Model Checking | [pdf] | [lec23] | ||||
| Thu 4/21 | Symbolic Model Checking | [lec24] | MP 2 (ckpt 4/22) | Further reading | |||
| Tue 4/26 | Model Checking with BDDs | [lec25] | Further reading | ||||
| Thu 4/28 | Review | [lec26] | MP 2 (due 4/29) | Practice Final [solution] | |||
| Tue 5/3 | Final Exam (1:00pm-4:00pm, GHC 4401) | [solution] |