Verified analysis of random binary tree structures. (English) Zbl 1468.68288

Avigad, Jeremy (ed.) et al., Interactive theorem proving. 9th international conference, ITP 2018, held as part of the federated logic conference, FloC 2018, Oxford, UK, July 9–12, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10895, 196-214 (2018).
Summary: 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.
For the entire collection see [Zbl 1391.68001].


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68P05 Data structures
68P10 Searching and sorting
68W20 Randomized algorithms
68W40 Analysis of algorithms
Full Text: DOI