FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
Verified Tail Bounds for Randomized Programs

Authors: Joseph Tassarotti and Robert Harper

Paper Information

Title:Verified Tail Bounds for Randomized Programs
Authors:Joseph Tassarotti and Robert Harper
Proceedings:ITP Papers
Editors: Jeremy Avigad and Assia Mahboubi
Keywords:randomized algorithm, probability, Master Theorem, formal verification, tail bound
Abstract:

ABSTRACT. We mechanize in Coq a theorem by Karp, along with several extensions, that provide an easy to use "cookbook" method for verifying tail bounds of randomized algorithms, much like the traditional "Master Theorem" gives bounds for deterministic algorithms. We apply these results to several examples: the number of comparisons performed by QuickSort, the span of parallel QuickSort, the height of randomly generated binary search trees, and the number of rounds needed for a distributed leader election protocol. Because the constants involved in our symbolic bounds are concrete, we are able to use them to derive numerical probability bounds for various input sizes for these examples.

Pages:19
Talk:Jul 12 16:00 (Session 78B)
Paper: