Verified Tail Bounds for Randomized Programs

Joseph Tassarotti; Robert Harper

doi:10.1007/978-3-319-94821-8_33

Verified Tail Bounds for Randomized Programs

Joseph Tassarotti, Robert Harper

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Abstract

We mechanize 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.

Original language	English (US)
Title of host publication	Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings
Editors	Jeremy Avigad, Assia Mahboubi
Publisher	Springer Verlag
Pages	560-578
Number of pages	19
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_33
State	Published - 2018
Event	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 - Oxford, United Kingdom Duration: Jul 9 2018 → Jul 12 2018

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10895 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018
Country/Territory	United Kingdom
City	Oxford
Period	7/9/18 → 7/12/18

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-319-94821-8_33

Cite this

Tassarotti, J., & Harper, R. (2018). Verified Tail Bounds for Randomized Programs. In J. Avigad, & A. Mahboubi (Eds.), Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings (pp. 560-578). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-319-94821-8_33

Verified Tail Bounds for Randomized Programs. / Tassarotti, Joseph; Harper, Robert.
Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. ed. / Jeremy Avigad; Assia Mahboubi. Springer Verlag, 2018. p. 560-578 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10895 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Tassarotti, J & Harper, R 2018, Verified Tail Bounds for Randomized Programs. in J Avigad & A Mahboubi (eds), Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10895 LNCS, Springer Verlag, pp. 560-578, 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 7/9/18. https://doi.org/10.1007/978-3-319-94821-8_33

Tassarotti J, Harper R. Verified Tail Bounds for Randomized Programs. In Avigad J, Mahboubi A, editors, Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. Springer Verlag. 2018. p. 560-578. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-94821-8_33

Tassarotti, Joseph ; Harper, Robert. / Verified Tail Bounds for Randomized Programs. Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings. editor / Jeremy Avigad ; Assia Mahboubi. Springer Verlag, 2018. pp. 560-578 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{748cc0b3059748769a8406c0f43a4f8f,

title = "Verified Tail Bounds for Randomized Programs",

abstract = "We mechanize 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.",

author = "Joseph Tassarotti and Robert Harper",

note = "Publisher Copyright: {\textcopyright} 2018, Springer International Publishing AG, part of Springer Nature.; 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018 ; Conference date: 09-07-2018 Through 12-07-2018",

year = "2018",

doi = "10.1007/978-3-319-94821-8_33",

language = "English (US)",

isbn = "9783319948201",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "560--578",

editor = "Jeremy Avigad and Assia Mahboubi",

booktitle = "Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings",

}

TY - GEN

T1 - Verified Tail Bounds for Randomized Programs

AU - Tassarotti, Joseph

AU - Harper, Robert

PY - 2018

Y1 - 2018

N2 - We mechanize 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.

AB - We mechanize 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.

UR - http://www.scopus.com/inward/record.url?scp=85049910120&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=85049910120&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-94821-8_33

DO - 10.1007/978-3-319-94821-8_33

M3 - Conference contribution

AN - SCOPUS:85049910120

SN - 9783319948201

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 560

EP - 578

BT - Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Proceedings

A2 - Avigad, Jeremy

A2 - Mahboubi, Assia

PB - Springer Verlag

T2 - 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018

Y2 - 9 July 2018 through 12 July 2018

ER -

Verified Tail Bounds for Randomized Programs

Abstract

Publication series

Conference

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this