Important note: This schedule is subject to change. I will try to keep it up to date, but please see Piazza for the latest information and homework deadlines.
| Week | Date | Topic | Readings & HW | Lecture # |
|---|---|---|---|---|
| 1 | April 1 | Introduction and demos | 0 | |
| April 3 | Hypothesis I: Specifications and correctness | Correctness (computer science) | 1 | |
| April 5 | Hypothesis II | Hypothesis docs | 1 | |
| 2 | April 8 | Hypothesis III: Complex specifications | HW0 due | 2 |
| April 10 | Hypothesis IV | 2 | ||
| April 12 | Hypothesis V: Limitations | 2 | ||
| 3 | April 15 | Z3 and Satisfiability | Z3 introduction | 3 |
| April 17 | Z3 II | Z3 docs | 3 | |
| April 19 | Z3 III | HW1 due | 3 | |
| 4 | April 22 | Z3 IV: Applications | 4 | |
| April 24 | Z3 V | 4 | ||
| April 26 | Z3 VI | 4 | ||
| 5 | April 29 | Z3 VII | 4 | |
| May 1 | Z3 VIII: Advanced | 5 | ||
| May 3 | Z3 IX | HW2 due | 5 | |
| 6 | May 6 | Z3 X | 5 | |
| May 8 | Z3 XII | 5 | ||
| May 10 | Z3 XIII: Internals and Limitations | 5 |
| Week | Date | Topic | Readings & HW | Lecture # |
|---|---|---|---|---|
| 7 | May 13 | Dafny I: Formal Verification | HW3 due | 6 |
| May 15 | Dafny II | 6 | ||
| May 17 | Dafny III | 6 | ||
| 8 | May 20 | Dafny IV | 6 | |
| May 22 | Dafny V | 7 | ||
| May 24 | Dafny VI | 7 | ||
| 9 | No Class (Memorial Day) | |||
| May 29 | Dafny VII | 7 | ||
| May 31 | Rust I: Safety Properties | 8 |
| Week | Date | Topic | Readings & HW | Lecture # |
|---|---|---|---|---|
| 10 | June 3 | Rust II | HW4 due | 8 |
| Last day of class -- June 5 | Course review | |||
| June 6 (Thursday) | HW5 due (optional) | |||
| 11 | June 10 | Last day to submit make-up assignments | ||
| Final -- June 12 |
Advanced topics1 was skipped due to time.
Footnotes
-
Possible advanced topics: polymorphism, concurrency, distributed systems, security properties ↩