CS 839: Systems Verification
This is a graduate-level class on systems verification: how to mathematically prove the correctness of programs with machine-checked proofs. A core technique throughout the class is separation logic, which we will use to reason about real-world programs written in Go, including using loop invariants, reasoning about slices, pointer-based data structures, and concurrency. Programming assignments will involve proving theorems with the Rocq prover.
Course info
Instructor: Tej Chajed ‹chajed@wisc.edu›
Lecture: Tue/Thu 1-2:15pm
Classroom: Morgridge Hall 2538
Office hours: Wed/Thu 3-4pm, in Morgridge 7572
We'll use Canvas for submitting assignments and Piazza for questions.
The source of this website is on GitHub at tchajed/sys-verif-fa25. Feel free to submit bug reports and PRs. Your fellow students as well as students in future iterations of this class will thank you!
Calendar
Note: consider anything two weeks or more away subject to change.
| Date | Lecture | Pre-reading | ||
|---|---|---|---|---|
| 1 | Thu Sep 4 | Introduction: notes, slides | ||
| 2 | Tue Sep 9 | Rocq introduction: notes | tool setup, course syllabus | bring a laptop |
| 3 | Thu Sep 11 | Induction | notes | |
| 4 | Tue Sep 16 | ADT specification | notes | |
| 5 | Thu Sep 18 | ADTs with invariants | notes | |
| 6 | Tue Sep 23 | Hoare logic (part 1) | notes | |
| 7 | Thu Sep 25 | Hoare logic (part 2) | ||
| Mon Sep 29 | Assignment 1 due (11pm) | |||
| 8 | Tue Sep 30 | Separation logic (part 1) | notes | |
| 9 | Thu Oct 2 | Separation logic (part 2) | ||
| 10 | Tue Oct 7 | Iris Proof Mode | notes | |
| 11 | Thu Oct 9 | Modeling Go programs | notes | |
| 12 | Tue Oct 14 | Loop invariants | notes | |
| 13 | Thu Oct 16 | Ownership | notes | |
| Mon Oct 20 | Assignment 2 due (11pm) | |||
| 14 | Tue Oct 21 | In-class work | ||
| 15 | Thu Oct 23 | Persistence | notes | |
| 16 | Tue Oct 28 | Concurrency intro | notes | |
| 17 | Thu Oct 30 | Lock invariants | notes | |
| 18 | Tue Nov 4 | Resource algebras | notes | |
| 19 | Tue Nov 6 | Ghost state | notes | |
| Mon Nov 10 | Assignment 3 due (11pm) | |||
| 20 | Tue Nov 11 | Atomic specs | notes | |
| 21 | Thu Nov 13 | Barrier proof (spec) | notes | |
| 22 | Tue Nov 18 | Barrier proof | ||
| 23 | Thu Nov 20 | Property-based testing | notes | |
| 24 | Tue Nov 25 | SMT-based verification | notes | |
| Thu Nov 27 | No class (Thanksgiving) | |||
| 25 | Tue Dec 2 | Liveness | notes | |
| 26 | Thu Dec 4 | slack | ||
| 27 | Tue Dec 9 | Course wrap-up | ||
| Thu Dec 11 | Assignment 4 due (11pm) |
Resources
See the resources page.
Note for instructors
If you're interested in this class please send me an email at chajed@wisc.edu. I'd love to hear what you think!
The course material (including this website) is licensed under the Creative Commons Attribution-NonCommercial 4.0 International License. See CC-BY-NC 4.0 for the text of the license.