{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T15:30:09Z","timestamp":1761060609751,"version":"3.40.3"},"publisher-location":"Cham","reference-count":53,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319948201"},{"type":"electronic","value":"9783319948218"}],"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_33","type":"book-chapter","created":{"date-parts":[[2018,7,3]],"date-time":"2018-07-03T13:25:55Z","timestamp":1530624355000},"page":"560-578","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Verified Tail Bounds for Randomized Programs"],"prefix":"10.1007","author":[{"given":"Joseph","family":"Tassarotti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Robert","family":"Harper","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,7,4]]},"reference":[{"key":"33_CR1","doi-asserted-by":"crossref","unstructured":"Affeldt, R., Hagiwara, M.: Formalization of Shannon\u2019s theorems in SSReflect-Coq. In: ITP, pp. 233\u2013249 (2012)","DOI":"10.1007\/978-3-642-32347-8_16"},{"issue":"2","key":"33_CR2","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1023\/A:1018373005182","volume":"10","author":"M Akra","year":"1998","unstructured":"Akra, M., Bazzi, L.: On the solution of linear recurrence equations. Comp. Opt. Appl. 10(2), 195\u2013210 (1998)","journal-title":"Comp. Opt. Appl."},{"issue":"8","key":"33_CR3","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":"33_CR4","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the Central Limit Theorem. CoRR abs\/1405.7012 (2014). http:\/\/arxiv.org\/abs\/1405.7012"},{"key":"33_CR5","doi-asserted-by":"crossref","unstructured":"Barthe, G., Crespo, J.M., Gr\u00e9goire, B., Kunz, C., B\u00e9guelin, S.Z.: Computer-aided cryptographic proofs. In: ITP, pp. 11\u201327 (2012)","DOI":"10.1007\/978-3-642-32347-8_2"},{"key":"33_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1007\/978-3-319-41528-4_3","volume-title":"Computer Aided Verification","author":"G Barthe","year":"2016","unstructured":"Barthe, G., Espitau, T., Ferrer Fioriti, L.M., Hsu, J.: Synthesizing probabilistic invariants via Doob\u2019s decomposition. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 43\u201361. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_3"},{"key":"33_CR7","unstructured":"Barthe, G., Espitau, T., Gr\u00e9goire, B., Hsu, J., Strub, P.: Proving uniformity and independence by self-composition and coupling. In: LPAR (2017)"},{"key":"33_CR8","unstructured":"Barthe, G., Gaboardi, M., Gr\u00e9goire, B., Hsu, J., Strub, P.: A program logic for union bounds. In: ICALP, pp. 107:1\u2013107:15 (2016)"},{"key":"33_CR9","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90\u2013101 (2009)","DOI":"10.1145\/1594834.1480894"},{"key":"33_CR10","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Probabilistic relational hoare logics for computer-aided security proofs. In: MPC, pp. 1\u20136 (2012)","DOI":"10.1007\/978-3-642-31113-0_1"},{"key":"33_CR11","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Hsu, J., Strub, P.: Coupling proofs are probabilistic product programs. In: POPL, pp. 161\u2013174 (2017)","DOI":"10.1145\/3093333.3009896"},{"issue":"1","key":"33_CR12","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s00453-002-1003-4","volume":"36","author":"L Bazzi","year":"2003","unstructured":"Bazzi, L., Mitter, S.K.: The solution of linear probabilistic recurrence relations. Algorithmica 36(1), 41\u201357 (2003)","journal-title":"Algorithmica"},{"issue":"3","key":"33_CR13","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1145\/1008861.1008865","volume":"12","author":"JL Bentley","year":"1980","unstructured":"Bentley, J.L., Haken, D., Saxe, J.B.: A general method for solving divide-and-conquer recurrences. SIGACT News 12(3), 36\u201344 (1980)","journal-title":"SIGACT News"},{"key":"33_CR14","doi-asserted-by":"crossref","unstructured":"Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL (2004)","DOI":"10.1145\/964001.964003"},{"key":"33_CR15","doi-asserted-by":"crossref","unstructured":"Blelloch, G., Greiner, J.: Parallelism in sequential functional languages. In: Proceedings of the 7th International Conference on Functional Programming Languages and Computer Architecture, pp. 226\u2013237 (1995)","DOI":"10.1145\/224164.224210"},{"issue":"1","key":"33_CR16","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"33_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"64","DOI":"10.1007\/978-3-319-63390-9_4","volume-title":"Computer Aided Verification","author":"Q Carbonneaux","year":"2017","unstructured":"Carbonneaux, Q., Hoffmann, J., Reps, T., Shao, Z.: Automated resource analysis with Coq proof objects. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 64\u201385. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_4"},{"key":"33_CR18","doi-asserted-by":"crossref","unstructured":"Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: POPL, pp. 467\u2013478 (2015)","DOI":"10.1145\/2813885.2737955"},{"key":"33_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"511","DOI":"10.1007\/978-3-642-39799-8_34","volume-title":"Computer Aided Verification","author":"A Chakarov","year":"2013","unstructured":"Chakarov, A., Sankaranarayanan, S.: Probabilistic program analysis with martingales. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 511\u2013526. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"33_CR20","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":"33_CR21","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160 (2017)","DOI":"10.1145\/3093333.3009873"},{"issue":"1","key":"33_CR22","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/S0304-3975(96)00261-7","volume":"181","author":"S Chaudhuri","year":"1997","unstructured":"Chaudhuri, S., Dubhashi, D.P.: Probabilistic recurrence relations revisited. Theor. Comput. Sci. 181(1), 45\u201356 (1997)","journal-title":"Theor. Comput. Sci."},{"key":"33_CR23","unstructured":"Cormen, T.H., Leiserson, C.E., Rivest, R.L., Stein, C.: Introduction to Algorithms, 3rd edn. MIT Press (2009). http:\/\/mitpress.mit.edu\/books\/introduction-algorithms"},{"issue":"3","key":"33_CR24","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s11334-010-0128-x","volume":"6","author":"M Daumas","year":"2010","unstructured":"Daumas, M., Lester, D., Martin-Dorel, \u00c9., Truffert, A.: Improved bound for stochastic formal correctness of numerical algorithms. Innovations Syst. Softw. Eng. 6(3), 173\u2013179 (2010)","journal-title":"Innovations Syst. Softw. Eng."},{"key":"33_CR25","doi-asserted-by":"crossref","unstructured":"Dubhashi, D.P., Panconesi, A.: Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press (2009). http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item2327542\/","DOI":"10.1017\/CBO9780511581274"},{"key":"33_CR26","unstructured":"Eberl, M.: Expected shape of random binary search trees. Archive of Formal Proofs 2017 (2017). https:\/\/www.isa-afp.org\/entries\/Random_BSTs.shtml"},{"key":"33_CR27","unstructured":"Eberl, M.: The number of comparisons in quicksort. Archive of Formal Proofs 2017 (2017). https:\/\/www.isa-afp.org\/entries\/Quick_Sort_Cost.shtml"},{"issue":"4","key":"33_CR28","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s10817-016-9378-0","volume":"58","author":"M Eberl","year":"2017","unstructured":"Eberl, M.: Proving divide and conquer complexities in Isabelle\/HOL. J. Autom. Reasoning 58(4), 483\u2013508 (2017)","journal-title":"J. Autom. Reasoning"},{"key":"33_CR29","unstructured":"Eberl, M., Haslbeck, M.W., Nipkow, T.: Verified analysis of random trees. In: ITP (2018)"},{"issue":"4","key":"33_CR30","doi-asserted-by":"publisher","first-page":"1260","DOI":"10.1214\/aoap\/1035463332","volume":"6","author":"JA Fill","year":"1996","unstructured":"Fill, J.A., Mahmoud, H.M., Szpankowski, W.: On the distribution for the duration of a randomized leader election algorithm. Ann. Appl. Probab. 6(4), 1260\u20131283 (1996)","journal-title":"Ann. Appl. Probab."},{"key":"33_CR31","doi-asserted-by":"crossref","unstructured":"Flajolet, P., Sedgewick, R.: Analytic Combinatorics. Cambridge University Press (2009)","DOI":"10.1017\/CBO9780511801655"},{"key":"33_CR32","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Research Report RR-6455, Inria Saclay Ile de France (2016). https:\/\/hal.inria.fr\/inria-00258384"},{"key":"33_CR33","unstructured":"Haslbeck, M.W., Eberl, M., Nipkow, T.: Treaps. Archive of Formal Proofs (2018). https:\/\/isa-afp.org\/entries\/Treaps.html"},{"key":"33_CR34","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J.: Formalising semantics for expected running time of probabilistic programs. In: ITP, pp. 475\u2013482 (2016)","DOI":"10.1007\/978-3-319-43144-4_30"},{"key":"33_CR35","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: ITP, pp. 135\u2013151 (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"33_CR36","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. Ph.D. thesis. Cambridge University, May 2003"},{"key":"33_CR37","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"},{"issue":"6","key":"33_CR38","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"},{"key":"33_CR39","unstructured":"Karpinski, M., Zimmermann, W.: Probabilistic recurrence relations for parallel divide-and-conquer algorithms. Technical report TR-91-067, International Computer Science Institute (ICSI) (1991). https:\/\/www.icsi.berkeley.edu\/ftp\/global\/pub\/techreports\/1991\/tr-91-067.pdf"},{"key":"33_CR40","doi-asserted-by":"crossref","unstructured":"Kozen, D.: A probabilistic PDL. In: STOC, pp. 291\u2013297 (1983)","DOI":"10.1145\/800061.808758"},{"issue":"3","key":"33_CR41","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/s10817-015-9350-4","volume":"57","author":"\u00c9 Martin-Dorel","year":"2016","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 57(3), 187\u2013217 (2016)","journal-title":"J. Autom. Reason."},{"key":"33_CR42","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). http:\/\/doi.acm.org\/10.1145\/3158121"},{"key":"33_CR43","doi-asserted-by":"crossref","unstructured":"Mitzenmacher, M., Upfal, E.: Probability and Computing - Randomized Algorithms and Probabilistic Analysis. Cambridge University Press (2005)","DOI":"10.1017\/CBO9780511813603"},{"issue":"3","key":"33_CR44","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. 18(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"33_CR45","doi-asserted-by":"crossref","unstructured":"Motwani, R., Raghavan, P.: Randomized Algorithms. Cambridge University Press (1995)","DOI":"10.1017\/CBO9780511814075"},{"key":"33_CR46","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"},{"issue":"1","key":"33_CR47","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1016\/0012-365X(93)90572-B","volume":"120","author":"H Prodinger","year":"1993","unstructured":"Prodinger, H.: How to select a loser. Disc. Math. 120(1), 149\u2013159 (1993)","journal-title":"Disc. Math."},{"key":"33_CR48","doi-asserted-by":"crossref","unstructured":"Ramsey, N., Pfeffer, A.: Stochastic lambda calculus and monads of probability distributions. In: POPL, pp. 154\u2013165 (2002)","DOI":"10.1145\/565816.503288"},{"key":"33_CR49","unstructured":"Ramshaw, L.H.: Formalizing the Analysis of Algorithms. Ph.D. thesis. Stanford University (1979)"},{"issue":"2","key":"33_CR50","doi-asserted-by":"publisher","first-page":"170","DOI":"10.1145\/375827.375837","volume":"48","author":"S Roura","year":"2001","unstructured":"Roura, S.: Improved master theorems for divide-and-conquer recurrences. J. ACM 48(2), 170\u2013205 (2001)","journal-title":"J. ACM"},{"key":"33_CR51","unstructured":"Tassarotti, J.: Probabilistic recurrence relations for work and span of parallel algorithms. CoRR abs\/1704.02061 (2017). http:\/\/arxiv.org\/abs\/1704.02061"},{"key":"33_CR52","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":"33_CR53","unstructured":"Young, N.: Answer to: Understanding proof of theorem 3.3 in Karp\u2019s probabilistic recurrence relations. Theoretical Computer Science Stack Exchange (2016). http:\/\/cstheory.stackexchange.com\/q\/37144"}],"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_33","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T05:03:42Z","timestamp":1571547822000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-94821-8_33"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319948201","9783319948218"],"references-count":53,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-94821-8_33","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"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"}}]}}