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/25 | Introduction | [pdf] | mystery.c0 | |||
| Thu 8/27 | Contracts | [pdf] | HW0 | mystery-live.c, mystery-live.mlw, mystery.c0, mystery.mlw | ||
| Tue 9/1 | Data Structures | [pdf] | mystery.mlw, queue.mlw | |||
| Thu 9/3 | Arrays and Ghosts | [pdf] | HW0 | HW1 | bitset.mlw, intset.mlw | |
| Tue 9/8 | Semantics | [pdf] | ||||
| Thu 9/10 | Semantics in Why3 | [pdf] | HW1 | HW2 | regexp.mlw | |
| Tue 9/15 | Dynamic Logic | [pdf] | ||||
| Thu 9/17 | Loops | [pdf] | HW2 | HW3 | ||
| Tue 9/22 | Arrays | [pdf] | ndl-v1.mlw | |||
| Thu 9/24 | Induction | [pdf] | HW3 | MP1 | ndl-v2.mlw | |
| Tue 9/29 | Convergence | [pdf] | ||||
| Thu 10/1 | Predicate Transformers | [pdf] | MP1 (chkpt) | |||
| Tue 10/6 | Project Day (no class) | |||||
| Thu 10/8 | Sequent Calculus | [pdf] | MP1 | array-theory.mlw | ||
| Tue 10/13 | Fall Break (no classes) | |||||
| Thu 10/15 | Fall Break (no classes) | |||||
| Tue 10/20 | Certificates | HW5 (released Monday 10/19) | ||||
| Thu 10/22 | Resolution | HW5 (due Sunday 10/25) | ||||
| Tue 10/27 | Equality and Uninterpreted Functions | |||||
| Thu 10/29 | Theory Combination | HW5 | HW6 | |||
| Tue 11/3 | Democracy Day (no classes) | |||||
| Thu 11/5 | Linear Temporal Logic | HW6 | MP2 | |||
| Tue 11/10 | LTL Model Checking | |||||
| Thu 11/12 | Branching Time Properties | MP2 (chkpt) | ||||
| Tue 11/17 | CTL Model Checking | |||||
| Thu 11/19 | Software and Bounded Model Checking | |||||
| Tue 11/24 | Project Day (no class) | MP2 | HW7 | |||
| Thu 11/26 | Thanksgiving Break (no classes) | |||||
| Tue 12/1 | Real World Verification | |||||
| Thu 12/3 | Final Review | HW7 |