Verified Analysis of Random Binary Tree Structures

Manuel Eberl; Max W. Haslbeck; Tobias Nipkow

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

Verified Analysis of Random Binary Tree Structures

Manuel Eberl
, Max W. Haslbeck
, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

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

4 Scopus citations

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, and the expected shape of a Treap. The last two 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.

Original language	English
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	196-214
Number of pages	19
ISBN (Print)	9783319948201
DOIs	https://doi.org/10.1007/978-3-319-94821-8_12
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: 9 Jul 2018 → 12 Jul 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	9/07/18 → 12/07/18

Access to Document

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

Cite this

Eberl, M., Haslbeck, M. W., & Nipkow, T. (2018). Verified Analysis of Random Binary Tree Structures. 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. 196-214). (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_12

Eberl, Manuel ; Haslbeck, Max W. ; Nipkow, Tobias. / Verified Analysis of Random Binary Tree Structures. 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. 196-214 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{2ac28e6185d34ee09105ccfcc8a18096,

title = "Verified Analysis of Random Binary Tree Structures",

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, and the expected shape of a Treap. The last two 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.",

author = "Manuel Eberl and Haslbeck, \{Max W.\} and Tobias Nipkow",

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\_12",

language = "English",

isbn = "9783319948201",

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

publisher = "Springer Verlag",

pages = "196--214",

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",

}

Eberl, M, Haslbeck, MW & Nipkow, T 2018, Verified Analysis of Random Binary Tree Structures. 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. 196-214, 9th International Conference on Interactive Theorem Proving, ITP 2018 Held as Part of the Federated Logic Conference, FloC 2018, Oxford, United Kingdom, 9/07/18. https://doi.org/10.1007/978-3-319-94821-8_12

Verified Analysis of Random Binary Tree Structures. / Eberl, Manuel; Haslbeck, Max W.; Nipkow, Tobias.
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. 196-214 (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 › peer-review

TY - GEN

T1 - Verified Analysis of Random Binary Tree Structures

AU - Eberl, Manuel

AU - Haslbeck, Max W.

AU - Nipkow, Tobias

PY - 2018

Y1 - 2018

N2 - 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, and the expected shape of a Treap. The last two 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.

AB - 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, and the expected shape of a Treap. The last two 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.

UR - https://www.scopus.com/pages/publications/85049871527

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

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

M3 - Conference contribution

AN - SCOPUS:85049871527

SN - 9783319948201

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

SP - 196

EP - 214

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 -

Eberl M, Haslbeck MW, Nipkow T. Verified Analysis of Random Binary Tree Structures. 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. 196-214. (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_12

Verified Analysis of Random Binary Tree Structures

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this