Schedule
Lecture notes 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 8/26 | Introduction | [pdf] | ||||
| Thu 8/28 | Contracts | [pdf] | HW0 | mystery.mlw | ||
| Tue 9/2 | Data Structures | [pdf] | queue.mlw | |||
| Thu 9/4 | Arrays and Ghosts | [pdf] | HW0 | HW1 | intset.mlw, bitset.mlw | |
| Tue 9/9 | Semantics | [pdf] | ||||
| Thu 9/11 | Semantics in Why3 | [pdf] | HW1 | HW2 | regexp.mlw | |
| Tue 9/16 | Dynamic Logic | |||||
| Thu 9/18 | Loops | HW2 | HW3 | |||
| Tue 9/23 | Arrays | |||||
| Thu 9/25 | Induction | HW3 | MP1 | |||
| Tue 9/30 | Convergence | |||||
| Thu 10/2 | Predicate Transformers | MP1 (chkpt) | ||||
| Tue 10/7 | Sequent Calculus | |||||
| Thu 10/9 | Project Day (no class) | MP1 | HW4 | |||
| Tue 10/14 | Fall Break (no classes) | |||||
| Thu 10/16 | Fall Break (no classes) | |||||
| Tue 10/21 | Resolution | |||||
| Thu 10/23 | Equality and Uninterpreted Functions | HW4 | HW5 | |||
| Tue 10/28 | Theory Combination | |||||
| Thu 10/30 | Linear Temporal Logic | HW5 | HW6 | |||
| Tue 11/4 | Democracy Day (no classes) | |||||
| Thu 11/6 | LTL Model Checking | HW6 | MP2 | |||
| Tue 11/11 | Branching Time Properties | |||||
| Thu 11/13 | CTL Model Checking | MP2 (chkpt) | ||||
| Tue 11/18 | Bounded Model Checking | |||||
| Thu 11/20 | Software Model Checking | |||||
| Tue 11/25 | Project Day (no class) | MP2 | HW7 | |||
| Thu 11/27 | Thanksgiving Break (no classes) | |||||
| Tue 12/2 | Real World Verification | |||||
| Thu 12/4 | Final Review | HW7 |