Skip to main content

Lecture 1: What is verification?
Lecture 2: Introduction to Coq
Lecture 3: Induction
Lecture 4: ADT specification
Lecture 5: ADTs with invariants
Lecture 6+7: Hoare Logic
Lecture 8+9: Separation Logic
Lecture 10: IPM
Lecture 11: Goose
Lecture 12: Loop invariants
Lecture 13: Ownership in Go
Lecture 15: Persistently
Lecture 16: Concurrency intro
Lecture 17: Lock invariants
Lecture 18: Resource Algebras
Lecture 19: Ghost state
Lecture 20: Atomic specs
Lecture 21+22: Barrier example
Lecture 24: PBT
Lecture 25: SMT verification
Lecture 26: Liveness
Lecture 27: Conclusion
Beyond this class
Ltac reference

Program Proofs

Catalog

Demo: binary search tree
Demo: stack data structure
Fractional permissions
Integers in GooseLang
What is decide?
Inputting special symbols
Named propositions
Notation
Types in GooseLang
Auth set ghost library
Demo: specifying and verifying a concurrent barrier
Demo: verifying fibonacci function

Beyond this class