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
Calendar
The schedule is still under construction. Consider anything more than ~2 weeks out to be subject to changes.
| 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 | Logic |
| 6 | Wed Sep 18 | Sets and maps |
| 7 | Mon Sep 23 | Specifying functional algorithms |
| 8 | Wed Sep 25 | Property-based testing |
| 9 | Mon Sep 30 | Proofs |
| Tue Oct 1 | Assignment 1 due (11pm) | |
| Part 2: Imperative programs | ||
| 10 | Wed Oct 2 | Modeling Go programs |
| 11 | Mon Oct 7 | Hoare logic |
| 12 | Wed Oct 9 | Separation logic |
| 13 | Mon Oct 14 | Iris Proof Mode |
| 14 | Wed Oct 16 | Go language features |
| 15 | Mon Oct 21 | Ownership |
| 16 | Wed Oct 23 | Examples |
| 17 | Mon Oct 28 | slack |
| Part 3: Concurrency | ||
| 18 | Wed Oct 30 | Concurrency intro |
| 19 | Mon Nov 4 | Ghost state |
| 20 | Wed Nov 6 | Modalities |
| 21 | Mon Nov 11 | Locks |
| 22 | Tue Nov 13 | Specifying atomic operations |
| 23 | Mon Nov 18 | Examples |
Tentatively, assignment 2 will be due Tue Oct 29 and assignment 3 will be due Tue Nov 5 (you're intended to work on these assignments in parallel; one is theory and the other is programming).