Overview
The basics
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
28.
Abstract predicates
Advanced topics
29.
Quantifier Triggers
30.
Magic Wands
31.
Mathematical types
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