Name
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 Martinez 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. |
Year | DOI | Venue |
|---|---|---|
2020 | 10.1007/s10817-020-09545-0 | JOURNAL OF AUTOMATED REASONING |
Keywords | Field | DocType |
Binary search trees,Randomised data structures,Randomised algorithms,Quicksort,Isabelle,Interactive theorem proving | Discrete mathematics,Algorithm,Random binary tree,Mathematics | Journal |
Volume | Issue | ISSN |
64.0 | SP5 | 0168-7433 |
Citations | PageRank | References |
0 | 0.34 | 0 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Manuel Eberl | 1 | 11 | 13.27 |
| Max W. Haslbeck | 2 | 0 | 0.68 |
| Tobias Nipkow | 3 | 3056 | 232.28 |