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 | |||||
| Thu 8/27 | Contracts | HW0 | ||||
| Tue 9/1 | Data Structures | |||||
| Thu 9/3 | Arrays and Ghosts | HW0 | HW1 | |||
| Tue 9/8 | Semantics | |||||
| Thu 9/10 | Semantics in Why3 | HW1 | HW2 | |||
| Tue 9/15 | Dynamic Logic | |||||
| Thu 9/17 | Loops | HW2 | HW3 | |||
| Tue 9/22 | Arrays | |||||
| Thu 9/24 | Induction | HW3 | MP1 | |||
| Tue 9/29 | Convergence | |||||
| Thu 10/1 | Predicate Transformers | MP1 (chkpt) | ||||
| Tue 10/6 | Sequent Calculus | |||||
| Thu 10/8 | Project Day (no class) | MP1 | HW4 | |||
| Tue 10/13 | Fall Break (no classes) | |||||
| Thu 10/15 | Fall Break (no classes) | |||||
| Tue 10/20 | Certificates | |||||
| Thu 10/22 | Equality and Uninterpreted Functions | HW4 | HW5 | |||
| Tue 10/27 | Theory Combination | |||||
| Thu 10/29 | Linear Temporal Logic | HW5 | HW6 | |||
| Tue 11/3 | Democracy Day (no classes) | |||||
| Thu 11/5 | LTL Model Checking | HW6 | MP2 | |||
| Tue 11/10 | Branching Time Properties | |||||
| Thu 11/12 | CTL Model Checking | MP2 (chkpt) | ||||
| Tue 11/17 | Bounded Model Checking | |||||
| Thu 11/19 | Software 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 |