{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:17:36Z","timestamp":1770279456399,"version":"3.49.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T00:00:00Z","timestamp":1581120000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T00:00:00Z","timestamp":1581120000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["NI 491\/16-1"],"award-info":[{"award-number":["NI 491\/16-1"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"FWF","award":["Y757"],"award-info":[{"award-number":["Y757"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2020,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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, the randomised binary search trees described by Mart\u00ednez 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.<\/jats:p>","DOI":"10.1007\/s10817-020-09545-0","type":"journal-article","created":{"date-parts":[[2020,2,8]],"date-time":"2020-02-08T11:02:21Z","timestamp":1581159741000},"page":"879-910","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Verified Analysis of Random Binary Tree Structures"],"prefix":"10.1007","volume":"64","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":[[2020,2,8]]},"reference":[{"key":"9545_CR1","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":"8","key":"9545_CR2","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). https:\/\/doi.org\/10.1016\/j.scico.2007.09.002","journal-title":"Sci. Comput. Program."},{"key":"9545_CR3","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1145\/1480881.1480894","DOI":"10.1145\/1480881.1480894"},{"key":"9545_CR4","doi-asserted-by":"publisher","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:\/\/doi.org\/10.1007\/978-3-662-49498-1_20. https:\/\/eprint.iacr.org\/2017\/753","DOI":"10.1007\/978-3-662-49498-1_20"},{"key":"9545_CR5","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Fu, H., Murhekar, A.: Automated recurrence analysis for almost-linear expected-runtime bounds. In: Computer Aided Verification: 29th International Conference, CAV 2017, pp. 118\u2013139 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_6","DOI":"10.1007\/978-3-319-63387-9_6"},{"key":"9545_CR6","unstructured":"Cicho\u0144, J.: Quick Sort: average complexity. http:\/\/cs.pwr.edu.pl\/cichon\/Math\/QSortAvg.pdf Accessed 13 Mar 2017"},{"key":"9545_CR7","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, New York (2001)","edition":"2"},{"key":"9545_CR8","unstructured":"Eberl, M.: Expected shape of random binary search trees. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Random_BSTs.html, Formal proof development"},{"key":"9545_CR9","unstructured":"Eberl, M.: The number of comparisons in QuickSort. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Quick_Sort_Cost.html, Formal proof development"},{"key":"9545_CR10","unstructured":"Eberl, M.: Randomised binary search trees. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Randomised_BSTs.html, Formal proof development"},{"key":"9545_CR11","doi-asserted-by":"publisher","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random trees. In: Proceedings of the 9th International Conference on Interactive Theorem Proving (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8","DOI":"10.1007\/978-3-319-94821-8"},{"key":"9545_CR12","doi-asserted-by":"publisher","unstructured":"Eberl, M., H\u00f6lzl, J., Nipkow, T.: A verified compiler for probability density functions. In: J.\u00a0Vitek (ed.) Proceedings of the 24th European Symposium on Programming, pp. 80\u2013104. Springer, Berlin Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46669-8_4","DOI":"10.1007\/978-3-662-46669-8_4"},{"key":"9545_CR13","doi-asserted-by":"publisher","unstructured":"Flajolet, P., Salvy, B., Zimmermann, P.: Lambda - Upsilon - Omega: An assistant algorithms analyzer. In: 6th International Conference Applied Algebra, Algebraic Algorithms and Error-Correcting Codes, AAECC-6, Rome, Italy, July 4\u20138, 1988, Proceedings, pp. 201\u2013212 (1988). https:\/\/doi.org\/10.1007\/3-540-51083-4_60","DOI":"10.1007\/3-540-51083-4_60"},{"key":"9545_CR14","doi-asserted-by":"publisher","unstructured":"Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, vol. 915, pp. 68\u201385. Springer Berlin (1982). https:\/\/doi.org\/10.1007\/BFb0092872","DOI":"10.1007\/BFb0092872"},{"key":"9545_CR15","unstructured":"Gou\u00ebzel, S.: Ergodic theory. Archive of Formal Proofs (2015). http:\/\/isa-afp.org\/entries\/Ergodic_Theory.html, Formal proof development"},{"key":"9545_CR16","unstructured":"Haslbeck, M., Eberl, M., Nipkow, T.: Treaps. Archive of Formal Proofs (2018). http:\/\/isa-afp.org\/entries\/Treaps.html, Formal proof development"},{"issue":"1","key":"9545_CR17","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). https:\/\/doi.org\/10.1093\/comjnl\/5.1.10","journal-title":"Comput. J."},{"key":"9545_CR18","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: J.C. Blanchette, S.\u00a0Merz (eds.) Interactive Theorem Proving (ITP 2016), pp. 475\u2013482. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-43144-4_30","DOI":"10.1007\/978-3-319-43144-4_30"},{"key":"9545_CR19","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9401-5","author":"J H\u00f6lzl","year":"2017","unstructured":"H\u00f6lzl, J.: Markov chains and Markov decision processes in Isabelle\/HOL. J. Autom. Reason. (2017). https:\/\/doi.org\/10.1007\/s10817-016-9401-5","journal-title":"J. Autom. Reason."},{"key":"9545_CR20","doi-asserted-by":"publisher","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: Interactive Theorem Proving\u2014Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22\u201325, 2011. Proceedings, pp. 135\u2013151 (2011). https:\/\/doi.org\/10.1007\/978-3-642-22863-6_12","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9545_CR21","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2002)"},{"key":"9545_CR22","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run\u2014times of probabilistic programs. In: Proceedings of the 25th European Symposium on Programming Languages and Systems: volume 9632, pp. 364\u2013389. Springer-Verlag New York, Inc., New York, NY, USA (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15","DOI":"10.1007\/978-3-662-49498-1_15"},{"issue":"6","key":"9545_CR23","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). https:\/\/doi.org\/10.1145\/195613.195632","journal-title":"J. ACM"},{"key":"9545_CR24","volume-title":"The Art of Computer Programming, Volume 3: Sorting and Searching","author":"DE Knuth","year":"1998","unstructured":"Knuth, D.E.: The Art of Computer Programming, Volume 3: Sorting and Searching. Addison Wesley Longman Publishing Co., Inc., Redwood City (1998)"},{"issue":"2","key":"9545_CR25","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). https:\/\/doi.org\/10.1016\/j.entcs.2005.10.030","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"9545_CR26","doi-asserted-by":"publisher","unstructured":"Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: P.\u00a0Thiemann (ed.) Programming Languages and Systems (ESOP 2016), LNCS, vol. 9632, pp. 503\u2013531. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-662-49498-1_20","DOI":"10.1007\/978-3-662-49498-1_20"},{"key":"9545_CR27","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/274787.274812","volume":"45","author":"C Mart\u00ednez","year":"1997","unstructured":"Mart\u00ednez, C., Roura, S.: Randomized binary search trees. J. ACM 45, 288 (1997)","journal-title":"J. ACM"},{"key":"9545_CR28","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/978-3-319-22102-1_21","volume-title":"Interactive Theorem Proving (ITP 2015). LNCS","author":"T Nipkow","year":"2015","unstructured":"Nipkow, T.: Amortized complexity verified. In: Urban, C., Zhang, X. (eds.) Interactive Theorem Proving (ITP 2015). LNCS, vol. 9236, pp. 310\u2013324. Springer, Berlin (2015)"},{"key":"9545_CR29","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-319-43144-4_19","volume-title":"Interactive Theorem Proving (ITP 2016), LNCS","author":"T Nipkow","year":"2016","unstructured":"Nipkow, T.: Automatic functional correctness proofs for functional search trees. In: Blanchette, J., Merz, S. (eds.) Interactive Theorem Proving (ITP 2016), LNCS, vol. 9807, pp. 307\u2013322. Springer, Berlin (2016)"},{"key":"9545_CR30","doi-asserted-by":"crossref","unstructured":"Nipkow, T.: Verified root-balanced trees. In: Chang, B.Y.E. (ed.) Asian Symposium on Programming Languages and Systems, APLAS 2017, LNCS, vol. 10695, pp. 255\u2013272. Springer, Berlin (2017)","DOI":"10.1007\/978-3-319-71237-6_13"},{"key":"9545_CR31","doi-asserted-by":"crossref","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, Berlin (2014)"},{"key":"9545_CR32","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"9545_CR33","doi-asserted-by":"publisher","unstructured":"Ottmann, T., Widmayer, P.: Algorithmen und Datenstrukturen, 5. Auflage. Spektrum Akademischer Verlag (2012). https:\/\/doi.org\/10.1007\/978-3-8274-2804-2","DOI":"10.1007\/978-3-8274-2804-2"},{"key":"9545_CR34","doi-asserted-by":"publisher","unstructured":"Petcher, A., Morrisett, G.: The foundational cryptography framework. In: R.\u00a0Focardi, A.C. Myers (eds.) Principles of Security and Trust: 4th International Conference, POST 2015, Lecture Notes in Computer Science, vol. 9036, pp. 53\u201372. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-662-46666-7_4","DOI":"10.1007\/978-3-662-46666-7_4"},{"issue":"3","key":"9545_CR35","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). https:\/\/doi.org\/10.1145\/765568.765571","journal-title":"J. ACM"},{"key":"9545_CR36","unstructured":"Schneider, J., Eberl, M., Lochbihler, A.: Monad normalisation. Archive of Formal Proofs (2017). http:\/\/isa-afp.org\/entries\/Monad_Normalisation.html, Formal proof development"},{"issue":"4","key":"9545_CR37","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). https:\/\/doi.org\/10.1007\/BF00289467","journal-title":"Acta Inf."},{"issue":"4","key":"9545_CR38","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). https:\/\/doi.org\/10.1007\/BF01940876","journal-title":"Algorithmica"},{"key":"9545_CR39","unstructured":"St\u00fcwe, D., Eberl, M.: Probabilistic primality testing. Archive of Formal Proofs (2019). http:\/\/isa-afp.org\/entries\/Probabilistic_Prime_Tests.html, Formal proof development"},{"key":"9545_CR40","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, Cham (2018)"},{"issue":"4","key":"9545_CR41","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). https:\/\/doi.org\/10.1145\/358841.358852","journal-title":"Commun. ACM"},{"key":"9545_CR42","first-page":"256","volume-title":"A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq","author":"E van der Weegen","year":"2009","unstructured":"van der Weegen, E., McKinna, J.: A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq, pp. 256\u2013271. Springer, Berlin (2009)"},{"key":"9545_CR43","unstructured":"Wenzel, M.: Isabelle\/Isar: 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":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09545-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-020-09545-0\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-020-09545-0.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,26]],"date-time":"2023-09-26T14:19:39Z","timestamp":1695737979000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-020-09545-0"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,2,8]]},"references-count":43,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2020,6]]}},"alternative-id":["9545"],"URL":"https:\/\/doi.org\/10.1007\/s10817-020-09545-0","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,2,8]]},"assertion":[{"value":"8 May 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 January 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 February 2020","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}