Verified Analysis of Random Binary Tree Structures

by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow

In: Proceedings of the 9th International Conference on Interactive Theorem Proving (2018)

DOI:

Abstract:

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.

Download preprint PDF (481 KiB)

@inproceedings{eberl18itp,
author="Eberl, Manuel and Haslbeck, Max W. and Nipkow, Tobias",
editor="Avigad, Jeremy and Mahboubi, Assia",
title="Verified Analysis of Random Binary Tree Structures",
booktitle="Interactive Theorem Proving",
year="2018",
publisher="Springer International Publishing (ITP 2018)",
series="Lecture Notes in Computer Science",
address="Cham",
pages="196--214",
doi="10.1007/978-3-319-94821-8_12",
isbn="978-3-319-94821-8"
}

Download BibTeX (449 Bytes)

(The final publication is available at link.springer.com)