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, and the expected shape of a
Treap. The last two 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.
pdf
BibTeX:
@inproceedings{EberlHN-ITP18,
author={Manuel Eberl, Max W. Haslbeck, Tobias Nipkow},
title={Verified Analysis of Random Binary Tree Structures},
booktitle={Interactive Theorem Proving (ITP 2018)},
editor={J. Avigad and A. Mahboubi},
publisher=Springer,series=LNCS,volume={10895},pages={196--214},year=2018}
Isabelle theories:
Quicksort
Random BSTs
Treaps