Program Proofs

Catalog

• Demos

  • 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

• Ltac reference

• Fractional permissions

• Goose tutorial

• Integers in GooseLang

• Types in GooseLang

• What is decide?

• Inputting special symbols

• Named propositions

• Notation