Verified Analysis of Random Binary Tree Structures (extended journal version)
by Manuel Eberl, Max W. Haslbeck, and Tobias Nipkow
In: J. Autom. Reasoning (2020)
DOI:
10.1007/s10817-020-09545-0Abstract:
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 Roura and Martinez, 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.
Note:
This is a revised and extended version of a 2018 ITP paper.
Download preprint PDF (549 KiB)
BibTeX:
@article{eberl20jar,
author="Eberl, Manuel and Haslbeck, Max W. and Nipkow, Tobias",
title="Verified Analysis of Random Binary Tree Structures",
journal="J. Autom. Reasoning",
year="2020",
month="feb",
day="08",
doi="10.1007/s10817-020-09545-0",
issn="1573-0670"
}
(The final publication is available at link.springer.com)