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

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

In: Journal of Automated Reasoning (2020)

DOI:

10.1007/s10817-020-09545-0

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,
  • 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:

@inproceedings{eberl19j,
author="Eberl, Manuel and Haslbeck, Max W. and Nipkow, Tobias",
title="Verified Analysis of Random Binary Tree Structures",
year="2019",
note="Draft available at \url{https://www21.in.tum.de/~eberlm/pdfs/random_trees_journal.pdf}"
}

Download BibTeX (258 Bytes)