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.

• What is verification?

• Introduction to Rocq

• Induction

• Model-based specifications for functional programs

• Hoare Logic (theory)

• Separation Logic (theory)

• Iris Proof Mode

• Goose - Modeling and reasoning about Go

• Loop invariants

• Goose - Ownership reasoning

• The persistently modality

• Concurrency introduction

• Lock invariants

• Resource Algebras

• Ghost state

• Atomic specifications

• Specification and Proof of a Concurrent Barrier

• Property-based testing (PBT)

• Automated verification with SMT

• Liveness

• Summary of the class

• Systems verification beyond this class

• Program Proofs

  • Demos
    Auth set ghost libraryDemo: specifying and verifying a concurrent barrierDemo: verifying fibonacci functionDemo: verifying a concurrent hashmapDemo: binary search treeDemo: stack data structure
  • Notation
  • Ltac reference
  • Fractional permissions
  • Goose tutorial
  • Named propositions
  • What is decide?
  • Inputting special symbols
  • Integers in GooseLang
  • Types in GooseLang