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 Martínez and Roura, 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.

Details

Title
Verified Analysis of Random Binary Tree Structures
Author
Eberl, Manuel 1   VIAFID ORCID Logo  ; Haslbeck, Max W 2   VIAFID ORCID Logo  ; Nipkow Tobias 1   VIAFID ORCID Logo 

1  Technische Universität Mönchen, Garching bei München, Germany (GRID:grid.6936.a) (ISNI:0000000123222966) 
2  University of Innsbruck, Innsbruck, Austria (GRID:grid.5771.4) (ISNI:0000 0001 2151 8122) 
Pages
879-910
Publication year
2020
Publication date
Jun 2020
Publisher
Springer Nature B.V.
ISSN
01687433
e-ISSN
15730670
Source type
Scholarly Journal
Language of publication
English
DOI
https://doi.org/10.1007/s10817-020-09545-0
ProQuest document ID
2427391956
Copyright
© The Author(s) 2020. This work is published under https://creativecommons.org/licenses/by/4.0/ (the “License”). Notwithstanding the ProQuest Terms and Conditions, you may use this content in accordance with the terms of the License.