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 | 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]
[video] |
|||
| 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 | [pdf] | HW6 | MP2 | eq-bv64.smt2 eq-bv512.smt2 eq-uf.smt2 color.smt2 |
| Tue 4/2 | Bounded Model Checking | [pdf] | cbmc-example.c | ||
| Thu 4/4 | Linear Temporal Logic | [pdf] | MP2 (chkpt) | vending.smv | |
| Tue 4/9 | Computation Tree Logic | [pdf] | ctl-vs-ltl.smv | ||
| Thu 4/11 | Carnival (no classes) | ||||
| Tue 4/16 | Review II | [pdf]
[video] |
23-review-slides-notes.pdf | ||
| Thu 4/18 | Project Day (no lecture) | MP2 | HW7 | ||
| Tue 4/23 | Real World Verification | [pdf] | |||
| Thu 4/25 | Theorem Proving in Lean | [pdf] | HW7 | demo.lean | |
| Mon 5/6 | Final Exam (8:30am-11:30am, GHC 4401) | reference-sheet.pdf |