Verified Analysis of Random Binary Tree Structures
by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
In: Proceedings of ITP 2018
DOI:
10.1007/978-3-319-94821-8_12Abstract:
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)
BibTeX:
@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"
}
(The final publication is available at link.springer.com)