Manuel Eberl, Max W. Haslbeck, Tobias Nipkow
Journal of Automated Reasoning 64, pp. 879 – 910, 2020.
pdf 
doi:10.1007/s10817-020-09545-0
Abstract
This work is a case study of the formal verification and complexity ana- lysis of some famous probabilistic algorithms and data structures in the proof assistant Isabelle/HOL. In particular, we consider the expected number of comparisons in ran- domised 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.
BibTex
@inproceedings{MEMHTN-JAR20, author = "Manuel Eberl and Max W. Haslbeck and Tobias Nipkow", title = "Verified Analysis of Random Binary Tree Structures", series = "J Autom Reasoning", volume = 64, pages = "879--910", year = 2020, doi = "10.1007/s10817-020-09545-0"}