Lecture notes
Lecture notes
These notes are the textbook of the class. I encourage you to read the lecture notes for a lecture afterward. The notes will include additional details and exercises that we won't get to in class.
Some chapters include a tag "literate" at the top. These are generated from Coq sources that are also distributed in the course exercises repo.
There are exercises throughout the notes, many with solutions. I highly recommend making an attempt at any exercise before looking at the solution, and if you're skimming to resist the temptation to open up the solutions. You'll learn much more by doing the exercises on your own than by passively reading. A small number of exericses are graded homework, but don't let that stop you from doing them and writing out the answers - and if you're unsure feel free to send me a solution and ask about it.
Lecture 1: What is verification?
Lecture 2: Introduction to Coq
Lecture 3: Induction
Lecture 4: Model-based specifications for functional programs
Lectures 6 and 7: Hoare Logic
Lectures 8 and 9: Separation Logic
Lecture 10: Iris Proof Mode
Lecture 11: Goose - Modeling and reasoning about Go
Lecture 12: Loop invariants
Lecture 13: Goose - Ownership reasoning
Lecture 15: The persistently modality
Lecture 16: Concurrency introduction
Lecture 17: Lock invariants
Lecture 18: Resource Algebras
Lecture 19: Ghost state
Lecture 20: Atomic specifications
Lecture 21 and 22: Specification and Proof of a Concurrent Barrier
Lecture 24: Property-based testing (PBT)
Lecture 25: Automated verification with SMT
Lecture 26: Liveness
Lecture 27: Conclusion
Systems verification beyond this class
Program Proofs
Ltac reference