Verified analysis of random binary tree structures. (English) Zbl 1468.68289

Summary: 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ínez 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.


68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68P05 Data structures
68P10 Searching and sorting
68W20 Randomized algorithms
68W40 Analysis of algorithms
Full Text: DOI


[1] 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
[2] Audebaud, P.; Paulin-Mohring, C., Proofs of randomized algorithms in Coq, Sci. Comput. Program., 74, 8, 568-589 (2009) · Zbl 1178.68667
[3] Barthe, G., Grégoire, B., Béguelin, 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-101 (2009). 10.1145/1480881.1480894 · Zbl 1315.68081
[4] Basin, D.A., Lochbihler, A., Sefidgar, S.R.: CryptHOL: Game-based proofs in higher-order logic. Cryptology ePrint Archive, Report 2017/753 (2017). 10.1007/978-3-662-49498-1_20. https://eprint.iacr.org/2017/753 · Zbl 1455.94121
[5] 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-139 (2017). 10.1007/978-3-319-63387-9_6
[6] Cichoń, J.: Quick Sort: average complexity. http://cs.pwr.edu.pl/cichon/Math/QSortAvg.pdf Accessed 13 Mar 2017
[7] Cormen, TH; Stein, C.; Rivest, RL; Leiserson, CE, Introduction to Algorithms (2001), New York: McGraw-Hill Higher Education, New York
[8] 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
[9] 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
[10] Eberl, M.: Randomised binary search trees. Archive of Formal Proofs (2018). http://isa-afp.org/entries/Randomised_BSTs.html, Formal proof development
[11] Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random trees. In: Proceedings of the 9th International Conference on Interactive Theorem Proving (2018). 10.1007/978-3-319-94821-8 · Zbl 1468.68288
[12] Eberl, M., Hölzl, J., Nipkow, T.: A verified compiler for probability density functions. In: J. Vitek (ed.) Proceedings of the 24th European Symposium on Programming, pp. 80-104. Springer, Berlin Heidelberg (2015). 10.1007/978-3-662-46669-8_4 · Zbl 1335.68037
[13] 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-8, 1988, Proceedings, pp. 201-212 (1988). 10.1007/3-540-51083-4_60 · Zbl 0681.68064
[14] Giry, M.: A categorical approach to probability theory. In: Categorical Aspects of Topology and Analysis, Lecture Notes in Mathematics, vol. 915, pp. 68-85. Springer Berlin (1982). 10.1007/BFb0092872 · Zbl 0486.60034
[15] Gouëzel, S.: Ergodic theory. Archive of Formal Proofs (2015). http://isa-afp.org/entries/Ergodic_Theory.html, Formal proof development
[16] Haslbeck, M., Eberl, M., Nipkow, T.: Treaps. Archive of Formal Proofs (2018). http://isa-afp.org/entries/Treaps.html, Formal proof development · Zbl 1468.68288
[17] Hoare, CAR, Quicksort, Comput. J., 5, 1, 10 (1962) · Zbl 0108.13601
[18] Hölzl, J.: Formalising semantics for expected running time of probabilistic programs. In: J.C. Blanchette, S. Merz (eds.) Interactive Theorem Proving (ITP 2016), pp. 475-482. Springer, Berlin (2016). 10.1007/978-3-319-43144-4_30 · Zbl 1478.68138
[19] Hölzl, J., Markov chains and Markov decision processes in Isabelle/HOL, J. Autom. Reason. (2017) · Zbl 1425.68375
[20] Hölzl, J., Heller, A.: Three chapters of measure theory in Isabelle/HOL. In: Interactive Theorem Proving—Second International Conference, ITP 2011, Berg en Dal, The Netherlands, August 22-25, 2011. Proceedings, pp. 135-151 (2011). 10.1007/978-3-642-22863-6_12 · Zbl 1342.68287
[21] Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, University of Cambridge (2002) · Zbl 1013.68193
[22] Kaminski, B.L., Katoen, J.P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected run—times of probabilistic programs. In: Proceedings of the 25th European Symposium on Programming Languages and Systems: volume 9632, pp. 364-389. Springer-Verlag New York, Inc., New York, NY, USA (2016). 10.1007/978-3-662-49498-1_15 · Zbl 1335.68058
[23] Karp, RM, Probabilistic recurrence relations, J. ACM, 41, 6, 1136-1150 (1994) · Zbl 0830.68046
[24] Knuth, DE, The Art of Computer Programming, Volume 3: Sorting and Searching (1998), Redwood City: Addison Wesley Longman Publishing Co., Inc., Redwood City
[25] Kwiatkowska, MZ; Norman, G.; Parker, D., Quantitative analysis with the probabilistic model checker PRISM, Electr. Notes Theor. Comput. Sci., 153, 2, 5-31 (2006)
[26] Lochbihler, A.: Probabilistic functions and cryptographic oracles in higher order logic. In: P. Thiemann (ed.) Programming Languages and Systems (ESOP 2016), LNCS, vol. 9632, pp. 503-531. Springer (2016). 10.1007/978-3-662-49498-1_20 · Zbl 1335.68033
[27] Martínez, C.; Roura, S., Randomized binary search trees, J. ACM, 45, 288 (1997) · Zbl 0904.68074
[28] Nipkow, T.; Urban, C.; Zhang, X., Amortized complexity verified, Interactive Theorem Proving (ITP 2015). LNCS, 310-324 (2015), Berlin: Springer, Berlin · Zbl 1465.68059
[29] Nipkow, T.; Blanchette, J.; Merz, S., Automatic functional correctness proofs for functional search trees, Interactive Theorem Proving (ITP 2016), LNCS, 307-322 (2016), Berlin: Springer, Berlin · Zbl 1478.68065
[30] 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-272. Springer, Berlin (2017)
[31] Nipkow, T.; Klein, G., Concrete Semantics with Isabelle/HOL (2014), Berlin: Springer, Berlin · Zbl 1410.68004
[32] Nipkow, T.; Paulson, L.; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[33] Ottmann, T., Widmayer, P.: Algorithmen und Datenstrukturen, 5. Auflage. Spektrum Akademischer Verlag (2012). 10.1007/978-3-8274-2804-2
[34] Petcher, A., Morrisett, G.: The foundational cryptography framework. In: R. Focardi, A.C. Myers (eds.) Principles of Security and Trust: 4th International Conference, POST 2015, Lecture Notes in Computer Science, vol. 9036, pp. 53-72. Springer (2015). 10.1007/978-3-662-46666-7_4
[35] Reed, B., The height of a random binary search tree, J. ACM, 50, 3, 306-332 (2003) · Zbl 1325.68076
[36] Schneider, J., Eberl, M., Lochbihler, A.: Monad normalisation. Archive of Formal Proofs (2017). http://isa-afp.org/entries/Monad_Normalisation.html, Formal proof development
[37] Sedgewick, R., The analysis of Quicksort programs, Acta Inf., 7, 4, 327-355 (1977) · Zbl 0325.68016
[38] Seidel, R.; Aragon, CR, Randomized search trees, Algorithmica, 16, 4, 464-497 (1996) · Zbl 0857.68030
[39] Stüwe, D., Eberl, M.: Probabilistic primality testing. Archive of Formal Proofs (2019). http://isa-afp.org/entries/Probabilistic_Prime_Tests.html, Formal proof development
[40] Tassarotti, J.; Harper, R.; Avigad, J.; Mahboubi, A., Verified tail bounds for randomized programs, Interactive Theorem Proving (2018), Cham: Springer, Cham · Zbl 06947002
[41] Vuillemin, J., A unifying look at data structures, Commun. ACM, 23, 4, 229-239 (1980) · Zbl 0434.68047
[42] van der Weegen, E.; McKinna, J., A Machine-Checked Proof of the Average-Case Complexity of Quicksort in Coq, 256-271 (2009), Berlin: Springer, Berlin · Zbl 1246.68201
[43] Wenzel, M.: Isabelle/Isar: a versatile environment for human-readable formal proof documents. Ph.D. thesis, Institut für Informatik, Technische Universität München (2002). https://mediatum.ub.tum.de/node?id=601724
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.