{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T16:24:47Z","timestamp":1776356687628,"version":"3.51.2"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319948201","type":"print"},{"value":"9783319948218","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-94821-8_12","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"196-214","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified Analysis of Random Binary Tree Structures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4263-6571","authenticated-orcid":false,"given":"Manuel","family":"Eberl","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9900-5746","authenticated-orcid":false,"given":"Max W.","family":"Haslbeck","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0730-515X","authenticated-orcid":false,"given":"Tobias","family":"Nipkow","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-319-22102-1_21","volume-title":"Interactive Theorem Proving","author":"T Nipkow","year":"2015","unstructured":"Nipkow, T.: Amortized complexity verified. In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 310\u2013324. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_21"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-43144-4_19","volume-title":"Interactive Theorem Proving","author":"T Nipkow","year":"2016","unstructured":"Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 307\u2013322. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_19"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1007\/978-3-319-71237-6_13","volume-title":"Programming Languages and Systems","author":"T Nipkow","year":"2017","unstructured":"Nipkow, T.: Verified root-balanced trees. In: Chang, B.-Y.E. (ed.) APLAS 2017. LNCS, vol. 10695, pp. 255\u2013272. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-71237-6_13"},{"key":"12_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"key":"12_CR5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics. With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics. With Isabelle\/HOL. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10542-0"},{"key":"12_CR6","unstructured":"Eberl, M.: The number of comparisons in QuickSort. Archive of Formal Proofs, Formal proof development, March 2017. http:\/\/isa-afp.org\/entries\/Quick_Sort_Cost.html"},{"key":"12_CR7","unstructured":"Eberl, M.: Expected shape of random binary search trees. Archive of Formal Proofs, Formal proof development, April 2017. http:\/\/isa-afp.org\/entries\/Random_BSTs.html"},{"key":"12_CR8","unstructured":"Haslbeck, M., Eberl, M., Nipkow, T.: Treaps. Archive of Formal Proofs, Formal proof development, March 2018. http:\/\/isa-afp.org\/entries\/Treaps.html"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_12"},{"key":"12_CR10","unstructured":"Gou\u00ebzel, S.: Ergodic theory. Archive of Formal Proofs, Formal proof development, December 2015. http:\/\/isa-afp.org\/entries\/Ergodic_Theory.html"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-662-46669-8_4","volume-title":"Programming Languages and Systems","author":"M Eberl","year":"2015","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 80\u2013104. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_4"},{"key":"12_CR12","doi-asserted-by":"publisher","first-page":"345","DOI":"10.1007\/s10817-016-9401-5","volume":"59","author":"J H\u00f6lzl","year":"2017","unstructured":"H\u00f6lzl, J.: Markov chains and Markov decision processes in Isabelle\/HOL. J. Autom. Reason. 59, 345\u2013387 (2017)","journal-title":"J. Autom. Reason."},{"key":"12_CR13","unstructured":"Basin, D.A., Lochbihler, A., Sefidgar, S.R.: Crypthol: game-based proofs in higher-order logic. Cryptology ePrint Archive, report 2017\/753 (2017). https:\/\/eprint.iacr.org\/2017\/753"},{"key":"12_CR14","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical Aspects of Topology and Analysis","author":"M Giry","year":"1982","unstructured":"Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68\u201385. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0092872"},{"issue":"1","key":"12_CR15","doi-asserted-by":"publisher","first-page":"10","DOI":"10.1093\/comjnl\/5.1.10","volume":"5","author":"CAR Hoare","year":"1962","unstructured":"Hoare, C.A.R.: Quicksort. Comput. J. 5(1), 10 (1962)","journal-title":"Comput. J."},{"issue":"4","key":"12_CR16","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/BF00289467","volume":"7","author":"R Sedgewick","year":"1977","unstructured":"Sedgewick, R.: The analysis of Quicksort programs. Acta Inf. 7(4), 327\u2013355 (1977)","journal-title":"Acta Inf."},{"key":"12_CR17","unstructured":"Cicho\u0144, J.: Quick Sort - average complexity. http:\/\/cs.pwr.edu.pl\/cichon\/Math\/QSortAvg.pdf"},{"key":"12_CR18","volume-title":"Introduction to Algorithms","author":"TH Cormen","year":"2001","unstructured":"Cormen, T.H., Stein, C., Rivest, R.L., Leiserson, C.E.: Introduction to Algorithms, 2nd edn. McGraw-Hill Higher Education, Boston (2001)","edition":"2"},{"key":"12_CR19","series-title":"Sorting and Searching","volume-title":"The Art of Computer Programming","author":"DE Knuth","year":"1998","unstructured":"Knuth, D.E.: The Art of Computer Programming. Sorting and Searching, vol. 3. Addison Wesley Longman Publishing Co., Redwood City (1998)"},{"key":"12_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-8274-2804-2","volume-title":"Algorithmen und Datenstrukturen","author":"T Ottmann","year":"2012","unstructured":"Ottmann, T., Widmayer, P.: Algorithmen und Datenstrukturen, 5th edn. Spektrum Akademischer Verlag, Auflage (2012)","edition":"5"},{"issue":"3","key":"12_CR21","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1145\/765568.765571","volume":"50","author":"B Reed","year":"2003","unstructured":"Reed, B.: The height of a random binary search tree. J. ACM 50(3), 306\u2013332 (2003)","journal-title":"J. ACM"},{"key":"12_CR22","unstructured":"Aslam, J.A.: A simple bound on the expected height of a randomly built binary search tree. Technical report TR2001-387, Dartmouth College, Hanover, NH (2001). Abstract and paper lost"},{"issue":"4","key":"12_CR23","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1145\/358841.358852","volume":"23","author":"J Vuillemin","year":"1980","unstructured":"Vuillemin, J.: A unifying look at data structures. Commun. ACM 23(4), 229\u2013239 (1980)","journal-title":"Commun. ACM"},{"issue":"4","key":"12_CR24","doi-asserted-by":"publisher","first-page":"464","DOI":"10.1007\/BF01940876","volume":"16","author":"R Seidel","year":"1996","unstructured":"Seidel, R., Aragon, C.R.: Randomized search trees. Algorithmica 16(4), 464\u2013497 (1996)","journal-title":"Algorithmica"},{"key":"12_CR25","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2002)"},{"issue":"8","key":"12_CR26","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"key":"12_CR27","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 90\u2013101 (2009)","DOI":"10.1145\/1480881.1480894"},{"key":"12_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-662-46666-7_4","volume-title":"Principles of Security and Trust","author":"A Petcher","year":"2015","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: Focardi, R., Myers, A. (eds.) POST 2015. LNCS, vol. 9036, pp. 53\u201372. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46666-7_4"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"503","DOI":"10.1007\/978-3-662-49498-1_20","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2016","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 503\u2013531. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_20"},{"key":"12_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-642-02444-3_16","volume-title":"Types for Proofs and Programs","author":"E Weegen van der","year":"2009","unstructured":"van der Weegen, E., McKinna, J.: A machine-checked proof of the average-case complexity of quicksort in Coq. In: Berardi, S., Damiani, F., de\u2019Liguoro, U. (eds.) TYPES 2008. LNCS, vol. 5497, pp. 256\u2013271. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02444-3_16"},{"key":"12_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/978-3-662-49498-1_15","volume-title":"Programming Languages and Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest Precondition reasoning for expected run\u2013times of probabilistic programs. In: Thiemann, P. (ed.) ESOP 2016. LNCS, vol. 9632, pp. 364\u2013389. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"key":"12_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/978-3-319-43144-4_30","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2016","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: Blanchette, J.C., Merz, S. (eds.) ITP 2016. LNCS, vol. 9807, pp. 475\u2013482. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_30"},{"key":"12_CR33","volume-title":"Interactive Theorem Proving","author":"J Tassarotti","year":"2018","unstructured":"Tassarotti, J., Harper, R.: Verified tail bounds for randomized programs. In: Avigad, J., Mahboubi, A. (eds.) Interactive Theorem Proving. Springer International Publishing, Cham (2018)"},{"issue":"6","key":"12_CR34","doi-asserted-by":"publisher","first-page":"1136","DOI":"10.1145\/195613.195632","volume":"41","author":"RM Karp","year":"1994","unstructured":"Karp, R.M.: Probabilistic recurrence relations. J. ACM 41(6), 1136\u20131150 (1994)","journal-title":"J. ACM"},{"issue":"2","key":"12_CR35","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1016\/j.entcs.2005.10.030","volume":"153","author":"MZ Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: Quantitative analysis with the probabilistic model checker PRISM. Electr. Notes Theor. Comput. Sci. 153(2), 5\u201331 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"12_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"201","DOI":"10.1007\/3-540-51083-4_60","volume-title":"Applied Algebra, Algebraic Algorithms and Error-Correcting Codes","author":"P Flajolet","year":"1989","unstructured":"Flajolet, P., Salvy, B., Zimmermann, P.: Lambda-Upsilon-Omega: an assistant algorithms analyzer. In: Mora, T. (ed.) AAECC 1988. LNCS, vol. 357, pp. 201\u2013212. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/3-540-51083-4_60"},{"key":"12_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-63387-9_6","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2017","unstructured":"Chatterjee, K., Fu, H., Murhekar, A.: Automated recurrence analysis for almost-linear expected-runtime bounds. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 118\u2013139. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_6"},{"key":"12_CR38","unstructured":"Wenzel, M.: Isabelle\/Isar \u2013 a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut f\u00fcr Informatik, Technische Universit\u00e4t M\u00fcnchen (2002). https:\/\/mediatum.ub.tum.de\/node?id=601724"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-94821-8_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T05:01:53Z","timestamp":1571547713000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]},"assertion":[{"value":"ITP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Interactive Theorem Proving","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Oxford","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2018","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 July 2018","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2018","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"itp2018","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/itp2018.inria.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}