Verified Analysis of Random Binary Tree Structures

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

In: Proceedings of ITP 2018

DOI:

Abstract:

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)

@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"
}

Download BibTeX (493 Bytes)

(The final publication is available at link.springer.com)