{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:23:25Z","timestamp":1770279805672,"version":"3.49.0"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031131875","type":"print"},{"value":"9783031131882","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,6]],"date-time":"2022-08-06T00:00:00Z","timestamp":1659744000000},"content-version":"vor","delay-in-days":217,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, we present the first fully-automated <jats:italic>expected amortised cost analysis<\/jats:italic> of self-adjusting data structures, that is, of <jats:italic>randomised splay trees<\/jats:italic>, <jats:italic>randomised splay heaps<\/jats:italic> and <jats:italic>randomised meldable heaps<\/jats:italic>, which so far have only (semi-)manually been analysed in the literature. Our analysis is stated as a type-and-effect system for a first-order functional programming language with support for sampling over discrete distributions, non-deterministic choice and a ticking operator. The latter allows for the specification of fine-grained cost models. We state two soundness theorems based on two different\u2014but strongly related\u2014typing rules of ticking, which account differently for the cost of non-terminating computations. Finally we provide a prototype implementation able to fully automatically analyse the aforementioned case studies.\"Image missing\"<\/jats:p>","DOI":"10.1007\/978-3-031-13188-2_4","type":"book-chapter","created":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:16:57Z","timestamp":1659687417000},"page":"70-91","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Automated Expected Amortised Cost Analysis of\u00a0Probabilistic Data Structures"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0391-3430","authenticated-orcid":false,"given":"Lorenz","family":"Leutgeb","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9240-6128","authenticated-orcid":false,"given":"Georg","family":"Moser","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1468-8398","authenticated-orcid":false,"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,6]]},"reference":[{"issue":"4","key":"4_CR1","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/S0020-0190(01)00230-7","volume":"81","author":"S Albers","year":"2002","unstructured":"Albers, S., Karpinski, M.: Randomized splay trees: theoretical and experimental results. IPL 81(4), 213\u2013221 (2002). https:\/\/doi.org\/10.1016\/S0020-0190(01)00230-7","journal-title":"IPL"},{"issue":"ICFP","key":"4_CR2","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3473592","volume":"5","author":"M Avanzini","year":"2021","unstructured":"Avanzini, M., Barthe, G., Lago, U.D.: On continuation-passing transformations and expected cost analysis. PACMPL 5(ICFP), 1\u201330 (2021). https:\/\/doi.org\/10.1145\/3473592","journal-title":"PACMPL"},{"key":"4_CR3","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Lago, U.D., Ghyselen, A.: Type-based complexity analysis of probabilistic functional programs. In: Proceedings of 34th LICS, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785725","DOI":"10.1109\/LICS.2019.8785725"},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"102338","DOI":"10.1016\/j.scico.2019.102338","volume":"185","author":"M Avanzini","year":"2020","unstructured":"Avanzini, M., Lago, U.D., Yamada, A.: On probabilistic term rewriting. Sci. Comput. Program. 185, 102338 (2020). https:\/\/doi.org\/10.1016\/j.scico.2019.102338","journal-title":"Sci. Comput. Program."},{"key":"4_CR5","doi-asserted-by":"publisher","unstructured":"Avanzini, M., Moser, G., Schaper, M.: A modular cost analysis for probabilistic programs. PACMPL 4(OOPSLA), 172:1\u2013172:30 (2020). https:\/\/doi.org\/10.1145\/3428240","DOI":"10.1145\/3428240"},{"key":"4_CR6","doi-asserted-by":"publisher","unstructured":"Barthe, G., Katoen, J.P., Silva, A. (eds.): Foundations of Probabilistic Programming. Cambridge University Press, Cambridge (2020). https:\/\/doi.org\/10.1017\/9781108770750","DOI":"10.1017\/9781108770750"},{"key":"4_CR7","doi-asserted-by":"publisher","unstructured":"Batz, K., Kaminski, B.L., Katoen, J., Matheja, C., Noll, T.: Quantitative separation logic: a logic for reasoning about probabilistic pointer programs. PACMPL 3(POPL), 34:1\u201334:29 (2019). https:\/\/doi.org\/10.1145\/3290347","DOI":"10.1145\/3290347"},{"key":"4_CR8","doi-asserted-by":"publisher","unstructured":"Blelloch, G.E., Reid-Miller, M.: Fast set operations using treaps. In: Proceedings of 10th SPAA, pp. 16\u201326 (1998). https:\/\/doi.org\/10.1145\/277651.277660","DOI":"10.1145\/277651.277660"},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/978-3-540-32033-3_24","volume-title":"Term Rewriting and Applications","author":"O Bournez","year":"2005","unstructured":"Bournez, O., Garnier, F.: Proving positive almost-sure termination. In: Giesl, J. (ed.) RTA 2005. LNCS, vol. 3467, pp. 323\u2013337. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-32033-3_24"},{"key":"4_CR10","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"},{"issue":"5","key":"4_CR11","doi-asserted-by":"publisher","first-page":"879","DOI":"10.1007\/s10817-020-09545-0","volume":"64","author":"M Eberl","year":"2020","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random binary tree structures. J. Autom. Reason. 64(5), 879\u2013910 (2020). https:\/\/doi.org\/10.1007\/s10817-020-09545-0","journal-title":"J. Autom. Reason."},{"key":"4_CR12","unstructured":"F\u00fcrer, M.: Randomized splay trees. In: Proceedings of 10th SODA, pp. 903\u2013904 (1999). http:\/\/dl.acm.org\/citation.cfm?id=314500.315079"},{"key":"4_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/3-540-49477-4_26","volume-title":"SOFSEM\u2019 98: Theory and Practice of Informatics","author":"A Gambin","year":"1998","unstructured":"Gambin, A., Malinowski, A.: Randomized meldable priority queues. In: Rovan, B. (ed.) SOFSEM 1998. LNCS, vol. 1521, pp. 344\u2013349. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/3-540-49477-4_26"},{"key":"4_CR14","doi-asserted-by":"publisher","unstructured":"Hofmann, M., Leutgeb, L., Moser, G., Obwaller, D., Zuleger, F.: Type-based analysis of logarithmic amortised complexity. MSCS (2021). https:\/\/doi.org\/10.1017\/S0960129521000232","DOI":"10.1017\/S0960129521000232"},{"key":"4_CR15","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. JACM 65(5), 30:1\u201330:68 (2018). https:\/\/doi.org\/10.1145\/3208102","DOI":"10.1145\/3208102"},{"issue":"3","key":"4_CR16","doi-asserted-by":"publisher","first-page":"328","DOI":"10.1016\/0022-0000(81)90036-2","volume":"22","author":"D Kozen","year":"1981","unstructured":"Kozen, D.: Semantics of probabilistic programs. J. Comput. Syst. Sci. 22(3), 328\u2013350 (1981)","journal-title":"J. Comput. Syst. Sci."},{"issue":"2","key":"4_CR17","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. JCSC 30(2), 162\u2013178 (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1","journal-title":"JCSC"},{"key":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-81688-9_5","volume-title":"Computer Aided Verification","author":"L Leutgeb","year":"2021","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: ATLAS: automated amortised complexity analysis of self-adjusting data structures. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12760, pp. 99\u2013122. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_5"},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Leutgeb, L., Moser, G., Zuleger, F.: Automated expected amortised cost analysis of probabilistic data structures. arXiv:2206.03537 (2022)","DOI":"10.1007\/978-3-030-81688-9_5"},{"issue":"2","key":"4_CR20","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1145\/274787.274812","volume":"45","author":"C Mart\u00ednez","year":"1998","unstructured":"Mart\u00ednez, C., Roura, S.: Randomized binary search trees. JACM 45(2), 288\u2013323 (1998). https:\/\/doi.org\/10.1145\/274787.274812","journal-title":"JACM"},{"key":"4_CR21","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. PACMPL 2(POPL), 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","DOI":"10.1145\/3158121"},{"key":"4_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"250","DOI":"10.1007\/978-3-030-72016-2_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F Meyer","year":"2021","unstructured":"Meyer, F., Hark, M., Giesl, J.: Inferring expected runtimes of probabilistic integer programs using expected sizes. In: TACAS 2021. LNCS, vol. 12651, pp. 250\u2013269. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_14"},{"key":"4_CR23","doi-asserted-by":"publisher","unstructured":"Mitzenmacher, M., Upfal, E.: Probability and Computing: Randomized Algorithms and Probabilistic Analysis. Cambridge University Press, Cambridge (2005). https:\/\/doi.org\/10.1017\/CBO9780511813603","DOI":"10.1017\/CBO9780511813603"},{"key":"4_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"491","DOI":"10.1007\/978-3-030-72019-3_18","volume-title":"Programming Languages and Systems","author":"M Moosbrugger","year":"2021","unstructured":"Moosbrugger, M., Bartocci, E., Katoen, J.-P., Kov\u00e1cs, L.: Automated termination analysis of polynomial probabilistic programs. In: ESOP 2021. LNCS, vol. 12648, pp. 491\u2013518. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72019-3_18"},{"key":"4_CR25","doi-asserted-by":"publisher","unstructured":"Motwani, R., Raghavan, P.: Randomized algorithms. In: Algorithms and Theory of Computation Handbook. Cambridge University Press (1999). https:\/\/doi.org\/10.1201\/9781420049503-c16","DOI":"10.1201\/9781420049503-c16"},{"key":"4_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"4_CR27","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Proceedings of 39th PLDI, pp. 496\u2013512 (2018). https:\/\/doi.org\/10.1145\/3192366.3192394","DOI":"10.1145\/3192366.3192394"},{"issue":"3","key":"4_CR28","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9459-3","volume":"62","author":"T Nipkow","year":"2019","unstructured":"Nipkow, T., Brinkop, H.: Amortized complexity verified. JAR 62(3), 367\u2013391 (2019)","journal-title":"JAR"},{"key":"4_CR29","volume-title":"Types and Programming Languages","author":"B Pierce","year":"2002","unstructured":"Pierce, B.: Types and Programming Languages. MIT Press, Cambridge (2002)"},{"issue":"6","key":"4_CR30","doi-asserted-by":"publisher","first-page":"668","DOI":"10.1145\/78973.78977","volume":"33","author":"W Pugh","year":"1990","unstructured":"Pugh, W.: Skip lists: a probabilistic alternative to balanced trees. CACM 33(6), 668\u2013676 (1990). https:\/\/doi.org\/10.1145\/78973.78977","journal-title":"CACM"},{"issue":"1","key":"4_CR31","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/0020-0190(93)90249-9","volume":"45","author":"B Schoenmakers","year":"1993","unstructured":"Schoenmakers, B.: A systematic analysis of splaying. IPL 45(1), 41\u201350 (1993)","journal-title":"IPL"},{"key":"4_CR32","unstructured":"Schoenmakers, B.: Data structures and amortized complexity in a functional setting. Ph.D. thesis, Eindhoven University of Technology (1992)"},{"key":"4_CR33","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)"},{"issue":"3","key":"4_CR34","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1145\/3828.3835","volume":"32","author":"D Sleator","year":"1985","unstructured":"Sleator, D., Tarjan, R.: Self-adjusting binary search trees. JACM 32(3), 652\u2013686 (1985)","journal-title":"JACM"},{"key":"4_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/978-3-030-01090-4_28","volume-title":"Automated Technology for Verification and Analysis","author":"T Takisaka","year":"2018","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in probabilistic programs. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 476\u2013493. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_28"},{"issue":"2","key":"4_CR36","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1137\/0606031","volume":"6","author":"R Tarjan","year":"1985","unstructured":"Tarjan, R.: Amortized computational complexity. SIAM J. Alg. Disc. Meth 6(2), 306\u2013318 (1985)","journal-title":"SIAM J. Alg. Disc. Meth"},{"key":"4_CR37","doi-asserted-by":"publisher","unstructured":"Wang, D., Kahn, D.M., Hoffmann, J.: Raising expectations: automating expected cost analysis with types. PACMPL 4(ICFP), 110:1\u2013110:31 (2020). https:\/\/doi.org\/10.1145\/3408992","DOI":"10.1145\/3408992"},{"key":"4_CR38","doi-asserted-by":"crossref","unstructured":"Wang, P., Fu, H., Goharshady, A.K., Chatterjee, K., Qin, X., Shi, W.: Cost analysis of nondeterministic probabilistic programs. In: Proceedings of 40th PLDI, pp. 204\u2013220. ACM (2019)","DOI":"10.1145\/3314221.3314581"},{"key":"4_CR39","doi-asserted-by":"publisher","unstructured":"Winskel, G.: The Formal Semantics of Programming Languages. FCS, MIT Press (1993). https:\/\/doi.org\/10.7551\/mitpress\/3054.003.0004","DOI":"10.7551\/mitpress\/3054.003.0004"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-13188-2_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,5]],"date-time":"2022-08-05T08:17:54Z","timestamp":1659687474000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-13188-2_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031131875","9783031131882"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-13188-2_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"6 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"34","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2022\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Double-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"209","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"40","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"11","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.9","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9.7","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}