Isabelle logo

Manuel Eberl

Chair for Logic and Verification

Verified Analysis of Random Binary Tree Structures

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

In: Proceedings of ITP 2018




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 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)


  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 (493 Bytes)

(The final publication is available at