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 | |
| Tue 2/4 | Dynamic Logic | [pdf] | ||||
| Thu 2/6 | Loops | [pdf] | HW2 | HW3 | ||
| Tue 2/11 | Arrays | [pdf] | ndl.mlw | |||
| Thu 2/13 | Induction | [pdf] | HW3 | MP1 | ndl.mlw | |
| Tue 2/18 | Convergence | [pdf] | ||||
| Thu 2/20 | Predicate Transformers | [pdf] | MP1 (chkpt) | |||
| Tue 2/25 | Sequent Calculus | [pdf] | ||||
| 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 | [pdf] | ||||
| Thu 3/13 | Propositional Encodings | [pdf] | HW4 | HW5 | ||
| Tue 3/18 | SAT Solving | [pdf] | ||||
| Thu 3/20 | SMT: Deciding EUF | [pdf] | HW5 | HW6 | ||
| Tue 3/25 | SMT: Theory Combination | [pdf] | ||||
| Thu 3/27 | SMT: Encodings | [pdf] | HW6 | MP2 | ||
| Tue 4/1 | Bounded Model Checking | [pdf] | ||||
| Thu 4/3 | Carnival (no classes) | |||||
| Tue 4/8 | Linear Temporal Logic | [pdf] | MP2 (chkpt) | |||
| Thu 4/10 | Computation Tree Logic | |||||
| 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 |