Verified Analysis of Random Binary Tree Structures

Abstract


This work is a case study of the formal verification and complexity ana- lysis of some famous probabilistic algorithms and data structures in the proof assistant Isabelle/HOL. In particular, we consider the expected number of comparisons in ran- domised 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.of the decision procedure for the first-order theory for a decidable class of rewrite systems. Besides its applications in research, this software pool has also proved invaluable for teaching, e.g., in multiple editions of the International Summer School on Rewriting.

Nach oben scrollen