Overview
Getting Started with Specifications and Verification
1.
Introduction
2.
Installation
3.
Basic specifications
4.
Verifying programs with arrays
5.
Quantifiers (forall, exists) and Implication (==>)
6.
Loops
6.1.
Loop Invariants
6.2.
Binary Search
6.3.
Range
7.
Overflow Checking
8.
Termination
9.
Ghost code
10.
Pure functions
Reasoning about Memory Accesses with Permissions
11.
Permission to write
12.
Self-framing assertions
13.
Addressability, @ and sharing
14.
Permission to read
14.1.
Wildcard permission
14.2.
Permission type and parameters
15.
Inhaling and exhaling
16.
Quantified permissions
17.
Pure functions and permissions
18.
Slices
19.
Maps
20.
Variadic functions
Abstraction and Information Hiding
21.
Predicates, fold, and unfold
22.
Abstracting memory access with predicates
23.
unfolding predicates
24.
Predicates and fractional permissions
25.
Abstraction functions
26.
Predicates as termination measures
27.
Full linked list example
Interfaces
28.
Behavioral subtypes
29.
nil interface values
30.
Type assertions, typeOf
31.
Abstracting memory with predicate interface members
32.
Implementation proofs (implements)
33.
Case study: sort.Interface
34.
Interfaces and termination
35.
Comparable interfaces, isComparable
36.
Full example: image
37.
The error interface
Concurrency
38.
Goroutines and data races
39.
First-class predicates
40.
Reasoning about mutual exclusion with sync.Mutex
41.
defer statements
42.
Share memory by communicating over channels
43.
Waiting on goroutines with sync.WaitGroup
Advanced topics
44.
Quantifier Triggers
45.
Magic Wands
46.
Mathematical types
47.
Playground
Light
Rust
Coal
Navy
Ayu
Practical Program Verification in Go with Gobra (alpha)
Triggers
TODO
Please refer to the Viper tutorial for now:
https://viper.ethz.ch/tutorial/#quantifiers