Verified Analysis of Random Binary Tree Structures
This work is a case study of the formal verification and complexity
analysis of some famous probabilistic algorithms and data structures
in the proof assistant Isabelle/HOL. In particular, we consider the
expected number of comparisons in randomised quicksort, the
relationship between randomised quicksort and average-case
deterministic quicksort, the expected shape of an unbalanced random
Binary Search Tree, the randomised binary search trees described by
Martínez and Roura, and the expected shape of a randomised treap. The
last three have, to our knowledge, not been analysed using a theorem
prover before and the last one is of particular interest because it
involves continuous distributions.
Springer link
BibTeX:
@article{EberlHN-JAR20,
author={Manuel Eberl, Max W. Haslbeck, Tobias Nipkow},
title={Verified Analysis of Random Binary Tree Structures},
journal={Journal of Automated Reasoning},
volume={64},number={5},pages={897--910},year=2020}
Isabelle theories:
Quicksort
Random BSTs
Treaps
Randomised Binary Search Trees
This is an extended version of this conference paper.