Schedule
This is a tentative schedule: we aim to produce reliable software, but the schedule is not reliable! Meanwhile, the current slides are here: slides.pdf.
| Date | Meeting Slides | Hands-On Material (Exam Bonus) | Quiz |
|---|---|---|---|
| 21.02 | Introduction | Dafny Intro | Q1 |
| 28.02 | Access Control and Cedar | Cedar | Q2 |
| 07.03 | Verified Programming with Dafny | Mini-Cedar in Dafny, part I | |
| 14.03 | Hoare Logic (Chad Nester) | Mini-Cedar in Dafny, part II | Q3 |
| 21.03 | Invariants | ||
| 28.03 | Collecting Semantics & Verification Conditions | Exercise (template) | |
| 04.04 | Coverage-Guided Fuzzing & Memory Vulnerabilities | Differential Testing | |
| 11.04 | When Dafny is not enough: Fstar (Danel Ahman) | ||
| 18.04 | (Good Friday - No Lecture) | ||
| 25.04 | Automated Software Verification | ||
| 02.05 | Abstract Interpretation | ||
| 09.05 | Type Systems for Low-Level Languages (Chad Nester) | ||
| 16.05 | Typed Assembly (Chad Nester) | ||
| 23.05 | Memory Safety (Chad Nester) | ||
| 30.05 | Conclusions (Chad Nester) |