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 | Exercise (template) | |
| 28.03 | Collecting Semantics & Verification Conditions | Exercise (template) | |
| 04.04 | Data Flow Analysis | Differential Testing & Coverage-Guided Fuzzing | |
| 11.04 | Assertion Checking | Exercise (template) | |
| 18.04 | (Good Friday - No Lecture) | ||
| 25.04 | Exercise Session (Karoliine Holter) | ||
| 02.05 | Low-Level Vulnerabilities | Infer | |
| 09.05 | Typed Assembly 1 (Chad Nester) | Notes | |
| 16.05 | Typed Assembly 2 (Chad Nester) | Notes | |
| 23.05 | Typed Assembly 3 (Chad Nester) | Notes | |
| 30.05 | Project Consultations |