Verified Analysis of Random Binary Tree Structures

Manuel Eberl, Max W. Haslbeck, Tobias Nipkow

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


author={Manuel Eberl, Max W. Haslbeck, Tobias Nipkow},
title={Verified Analysis of Random Binary Tree Structures},
journal={Journal of Automated Reasoning},

Isabelle theories: Quicksort Random BSTs Treaps Randomised Binary Search Trees

This is an extended version of this conference paper.