Program Proofs

These notes serve as a reference for writing program proofs. Compared to the main lecture notes, these focus on practical information you need while writing proofs, without exercises or much exposition about the motivation.

• Decidable equality

• Fractional permissions

• Goose tutorial

• Inputting special symbols

• Types in Perennial and Goose

• Ltac reference

• Integers in GooseLang

• Named propositions

• Notation

• Demos

  • Demo: proofs of simple Go code
  • Demo: verifying fibonacci function
  • Demo: binary search tree
  • Demo: FastExp loop invariant
  • Demo: stack data structure
  • Demo: verifying a concurrent hashmap
  • Auth set ghost library
  • Demo: specifying and verifying a concurrent barrier