CS 839: Systems Verification
Website subject to change
This website was copied from the 2025 iteration of the class and is still under construction. The lectures and especially assignments are still subject to change.
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 for Fall 2026
Instructor: Tej Chajed ‹chajed@wisc.edu›
Lecture: Mon/Wed 1-2:15pm
Classroom: Morgridge Hall 2538
We'll use Canvas for submitting assignments and Piazza for questions.
The source of this website is on GitHub at tchajed/sys-verif-fa26. 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: this is still subject to some substantial changes.
The hand-written iPad notes 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 (part 1) | notes | |
| 15 | Thu Oct 30 | Loop invariants (part 2) | same notes | |
| 16 | Tue Nov 4 | Persistence | notes | |
| 17 | Thu Nov 6 | Concurrency intro: slides | notes | |
| 18 | Tue Nov 11 | Lock invariants: slides | notes | |
| 19 | Thu Nov 13 | Ghost state | notes | |
| Mon Nov 17 | Assignment 3 due (11pm) | |||
| 20 | Tue Nov 18 | Atomic specs (part 1) | notes | |
| 21 | Thu Nov 20 | Atomic specs (part 2) | same notes (also hashmap demo) | |
| 22 | Tue Nov 25 | In-class work | assignment 4 | bring a laptop |
| Thu Nov 27 | No class (Thanksgiving) | |||
| 23 | Tue Dec 2 | Property-based testing | notes | |
| 24 | Thu Dec 4 | Liveness | notes | |
| 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.