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: Mon/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: plans two weeks out might change.
The hand-written iPad notes (for lectures 1-8) are available at board-notes.pdf.
| Date | Lecture | Reading | ||
|---|---|---|---|---|
| 1 | Thu Sep 4 | Introduction: slides | notes | |
| 2 | Tue Sep 9 | Rocq introduction: slides | notes, syllabus | bring a laptop and follow setup |
| 3 | Thu Sep 11 | Induction: slides | notes | |
| 4 | Tue Sep 16 | Abstraction: slides | notes | |
| 5 | Thu Sep 18 | Hoare logic (part 1): slides | notes | theory lecture |
| 6 | Tue Sep 23 | Hoare logic (part 2): slides | same notes | theory lecture |
| 7 | Thu Sep 25 | Separation logic (part 1): slides | notes | theory lecture |
| Mon Sep 29 | Assignment 1 due (11pm) | |||
| 8 | Tue Sep 30 | Separation logic (part 2): slides | same notes | theory lecture |
| Thu Oct 2 | No class (Tej is traveling) | |||
| 9 | Tue Oct 7 | Iris Proof Mode (part 1) | notes | bring a laptop |
| Thu Oct 9 | No class (Tej is sick) | |||
| 10 | Tue Oct 14 | Iris Proof Mode (part 2) | same notes | bring a laptop |
| 11 | Thu Oct 16 | Modeling Go programs: slides | notes | |
| Mon Oct 20 | Assignment 2 due (11pm) | |||
| 12 | Tue Oct 21 | Ownership (part 1) | notes | bring a laptop |
| 13 | Thu Oct 23 | Ownership (part 2) | same notes | bring a laptop |
| 14 | Tue Oct 28 | Loop invariants | notes | |
| 15 | Thu Oct 30 | Persistence | notes | |
| 16 | Tue Nov 4 | Concurrency intro | notes | |
| 17 | Thu Nov 6 | Lock invariants | notes | |
| Mon Nov 10 | Assignment 3 due (11pm) | |||
| 18 | Tue Nov 11 | Ghost state | notes | |
| 19 | Thu Nov 13 | Atomic specs | notes | |
| 20 | Tue Nov 18 | Barrier proof (spec) | notes | |
| 21 | Thu Nov 20 | Barrier proof | ||
| 22 | Tue Nov 25 | Property-based testing | notes | |
| Thu Nov 27 | No class (Thanksgiving) | |||
| 23 | Tue Dec 2 | Liveness | notes | |
| 24 | Thu Dec 4 | slack | ||
| 25 | Tue Dec 9 | Course wrap-up | notes | |
| 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.