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 Coq proof assistant.
Course info
Instructor: Tej Chajed ‹chajed@wisc.edu›
Office: CS 7361
Office hours: Mon/Wed 2-3pm
Lecture: Mon/Wed 9:30-10:45am
Classroom: Engineering Hall 2349
We'll use Canvas for submitting assignments and Piazza for questions (or email me).
The source of this website is on GitHub at tchajed/sys-verif-fa24. You can open an Issue or use Discussions if anything is confusing about the lecture notes, or post on Piazza. Your fellow students as well as students in future iterations of this class will thank you!
Resources
See the course lecture notes and the resources page.
Calendar
| Day | Lecture | |
|---|---|---|
| 1 | Wed Sep 4 | Introduction |
| Part 1: Functional programs | ||
| 2 | Mon Sep 9 | Coq introduction |
| 3 | Wed Sep 11 | Induction |
| 4 | Mon Sep 16 | ADT specification |
| 5 | Wed Sep 18 | ADTs with invariants |
| Part 2: Imperative programs | ||
| 6 | Mon Sep 23 | Hoare logic (part 1) |
| 7 | Wed Sep 25 | Hoare logic (part 2) |
| 8 | Mon Sep 30 | Separation logic (part 1) |
| Tue Oct 1 | Assignment 1 due (11pm) | |
| 9 | Wed Oct 2 | Separation logic (part 2) |
| 10 | Mon Oct 7 | Iris Proof Mode |
| 11 | Wed Oct 9 | Modeling Go programs |
| 12 | Mon Oct 14 | Loop invariants |
| 13 | Wed Oct 16 | Ownership |
| 14 | Mon Oct 21 | In-class work |
| Tue Oct 22 | Assignment 2 due (11pm) | |
| 15 | Wed Oct 23 | Persistence |
| Part 3: Concurrency | ||
| 16 | Mon Oct 28 | Concurrency intro |
| 17 | Wed Oct 30 | Lock invariants |
| 18 | Mon Nov 4 | No class |
| 19 | Wed Nov 6 | No class |
| 18 | Mon Nov 11 | Resource algebras |
| 19 | Wed Nov 13 | Ghost state |
| Thu Nov 14 | Assignment 3 due (11pm) | |
| 20 | Mon Nov 18 | Atomic specs |
| 21 | Wed Nov 20 | Barrier proof (spec) |
| 22 | Mon Nov 25 | Barrier proof |
| 23 | Wed Nov 27 | In-class work |
| 24 | Mon Dec 2 | Property-based testing |
| 25 | Wed Dec 4 | SMT-based verification |
| 26 | Mon Dec 9 | Liveness |
| 27 | Wed Dec 11 | Course wrap-up |
| Mon Dec 16 | Assignment 4 due (11pm) |
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.