Verified Root-Balanced Trees
Andersson introduced general balanced trees, search trees based on the design principle of partial rebuilding: perform update operations naively until the tree becomes too unbalanced, at which point you rebalance a whole subtree. We define and analyze a functional version of general balanced trees which we call root-balanced trees. Using a lightweight model of execution time, amortized logarithmic complexity is verified in the theorem prover Isabelle. Experimental results show competitiveness of root-balanced with AVL and red-black trees.
pdf
BibTeX:
@InProceedings{Nipkow-APLAS17,
author ={Tobias Nipkow},
title ={Verified Root-Balanced Trees},
booktitle ={Asian Symposium on Programming Languages and Systems, APLAS 2017},
pages ={255--272},
series ={LNCS},
year ={2017},
volume ={10695},
editor ={Bor-Yuh Evan Chang},
publisher ={Springer},
}
Online article
Isabelle theories in the
Archive of Formal Proofs