AVL trees
Automatically verified implementation of data structures based on AVL trees. This implementation and the proofs are presented in the paper Automatically verified implementation of data structures based on AVL trees.
Authors: Martin Clochard
Topics: Trees / Data Structures
Tools: Why3
see also the index (by topic, by tool, by reference, by year)
This example is split into several files.