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 1/14 | Introduction | [pdf] | ||||
| Thu 1/16 | Contracts | [pdf] | HW0 | mystery.mlw | ||
| Tue 1/21 | Data Structures | [pdf] | queue.mlw | |||
| Thu 1/23 | Arrays and Ghosts | [pdf] | HW0 | HW1 | queue.mlw negate.mlw bitset.mlw | |
| Tue 1/28 | Semantics | [pdf] | ||||
| Thu 1/30 | Semantics in Why3 | [pdf] | HW1 | HW2 | regexp.mlw | |
| Thu 2/4 | Dynamic Logic | HW1 | HW2 | |||
| Tue 2/6 | Loops | |||||
| Thu 2/11 | Arrays | HW2 | HW3 | |||
| Tue 2/13 | Induction | |||||
| Thu 2/18 | Diamonds | HW3 | MP1 | |||
| Thu 2/20 | Strongest Postconditions | MP1 (chkpt) | ||||
| Tue 2/25 | Sequent Calculus | |||||
| Thu 2/27 | Project Day (no class) | MP1 | HW4 | |||
| Th 3/4 | Spring Break (no classes) | |||||
| Thu 3/6 | Spring Break (no classes) | |||||
| Tue 3/11 | Resolution | |||||
| Thu 3/13 | Propositional Encodings | HW4 | HW5 | |||
| Tue 3/18 | SAT Solving | |||||
| Thu 3/20 | SMT: Deciding EUF | HW5 | HW6 | |||
| Tue 3/25 | SMT: Nelson-Oppen | |||||
| Thu 3/27 | SMT: Encodings | HW6 | MP2 | |||
| Tue 4/1 | Bounded Model Checking | |||||
| Thu 4/3 | Carnival (no classes) | |||||
| Tue 4/8 | Linear Temporal Logic | |||||
| Thu 4/10 | Computation Tree Logic | MP2 (chkpt) | ||||
| Tue 4/15 | Review 2 | |||||
| Thu 4/17 | Project day (no class) | MP2 | HW7 | |||
| Tue 4/22 | Real World Verification | |||||
| Thu 4/24 | Theorem Proving | HW7 |