Skip to main content

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

Demos

10/26/25

Last Updated10/26/25, 4:02 PM