Skip to main content

What is verification?
Introduction to Rocq
Induction
ADT specification
ADTs with invariants
Hoare Logic
Separation Logic
IPM
Goose
Loop invariants
Ownership in Go
Persistently
Concurrency intro
Lock invariants
Resource Algebras
Ghost state
Atomic specs
Barrier example
PBT
SMT verification
Liveness
Summary
Beyond this class

Demos

Catalog

Auth set ghost library
Demo: specifying and verifying a concurrent barrier
Demo: verifying fibonacci function
Demo: verifying a concurrent hashmap
Demo: binary search tree
Demo: stack data structure

Fractional permissions