Simpler Proofs with Decentralized Invariants
These are the Why3 source files for
the verified programs described in the paper
Simpler Proofs with
Decentralized Invariants
(Jean-Christophe
Filliâtre, Journal of Logical and Algebraic Methods in
Programming, January 2021). Also
available here.
These proofs were prepared using Why3 version 1.3.1.
- Union-find
- Heap-based prioriy queue
- Inverse of a permutation