Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Verified Analysis of Random Binary Tree Structures (extended journal version, unpublished draft)

by Manuel Eberl, Max W. Haslbeck, and 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 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.


This is a revised and extended version of a 2018 ITP paper.

Download draft PDF (549 KiB)


author="Eberl, Manuel and Haslbeck, Max W. and Nipkow, Tobias",
title="Verified Analysis of Random Binary Tree Structures",
note="Draft available at \url{}"

Download BibTeX (258 Bytes)