{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:18Z","timestamp":1780994658796,"version":"3.54.1"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030174644","type":"print"},{"value":"9783030174651","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","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":[[2019]]},"DOI":"10.1007\/978-3-030-17465-1_8","type":"book-chapter","created":{"date-parts":[[2019,4,3]],"date-time":"2019-04-03T22:50:37Z","timestamp":1554331837000},"page":"135-153","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":33,"title":["Tail Probabilities for Randomized Program Runtimes via Martingales for Higher Moments"],"prefix":"10.1007","author":[{"given":"Satoshi","family":"Kura","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Natsuki","family":"Urabe","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2019,4,3]]},"reference":[{"issue":"POPL","key":"8_CR1","first-page":"34:1","volume":"2","author":"S Agrawal","year":"2018","unstructured":"Agrawal, S., Chatterjee, K., Novotn\u00fd, P.: Lexicographic ranking supermartingales: an efficient approach to termination of probabilistic programs. PACMPL 2(POPL), 34:1\u201334:32 (2018)","journal-title":"PACMPL"},{"key":"8_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"186","DOI":"10.1007\/978-3-319-89884-1_7","volume-title":"Programming Languages and Systems","author":"K Batz","year":"2018","unstructured":"Batz, K., Kaminski, B.L., Katoen, J.-P., Matheja, C.: How long, O Bayesian network, will I sample thee? - A program analysis perspective on expected sampling times. In: Ahmed, A. (ed.) ESOP 2018. LNCS, vol. 10801, pp. 186\u2013213. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89884-1_7"},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1093\/acprof:oso\/9780199535255.001.0001","volume-title":"Concentration Inequalities: A Nonasymptotic Theory of Independence","author":"S Boucheron","year":"2013","unstructured":"Boucheron, S., Lugosi, G., Massart, P.: Concentration Inequalities: A Nonasymptotic Theory of Independence. Oxford University Press, Oxford (2013)"},{"key":"8_CR4","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). \n                      https:\/\/doi.org\/10.1007\/978-3-642-39799-8_34"},{"key":"8_CR5","unstructured":"Chatterjee, K., Fu, H.: Termination of nondeterministic recursive probabilistic programs. CoRR, abs\/1701.02944 (2017)"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-319-41528-4_1","volume-title":"Computer Aided Verification","author":"K Chatterjee","year":"2016","unstructured":"Chatterjee, K., Fu, H., Goharshady, A.K.: Termination analysis of probabilistic programs through Positivstellensatz\u2019s. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 3\u201322. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-41528-4_1"},{"issue":"2","key":"8_CR7","doi-asserted-by":"publisher","first-page":"7:1","DOI":"10.1145\/3174800","volume":"40","author":"K Chatterjee","year":"2018","unstructured":"Chatterjee, K., Fu, H., Novotn\u00fd, P., Hasheminezhad, R.: Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs. ACM Trans. Program. Lang. Syst. 40(2), 7:1\u20137:45 (2018)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"8_CR8","doi-asserted-by":"crossref","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: POPL, pp. 145\u2013160. ACM (2017)","DOI":"10.1145\/3093333.3009873"},{"issue":"2","key":"8_CR9","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1137\/S0895479804442462","volume":"27","author":"T Dayar","year":"2005","unstructured":"Dayar, T., Akar, N.: Computing moments of first passage times to a subset of states in markov chains. SIAM J. Matrix Anal. Appl. 27(2), 396\u2013412 (2005)","journal-title":"SIAM J. Matrix Anal. Appl."},{"key":"8_CR10","unstructured":"Doerr, B.: Probabilistic tools for the analysis of randomized optimization heuristics. CoRR, abs\/1801.06733 (2018)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Ferrer Fioriti, L.M., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: POPL, pp. 489\u2013501. ACM (2015)","DOI":"10.1145\/2775051.2677001"},{"key":"8_CR12","unstructured":"The GNU linear programming kit. \n                      https:\/\/www.gnu.org\/software\/glpk\/"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Jagtap, P., Soudjani, S., Zamani, M.: Temporal logic verification of stochastic systems using barrier certificates. In: Lahiri and Wang [24], pp. 177\u2013193","DOI":"10.1007\/978-3-030-01090-4_11"},{"key":"8_CR14","unstructured":"Jansson, C.: Termination and verification for ill-posed semidefinite programming problems. Optimization Online (2005)"},{"key":"8_CR15","unstructured":"Jansson, C.: VSDP: a MATLAB software package for verified semidefinite programming. In: NOLTA, pp. 327\u2013330 (2006)"},{"issue":"1","key":"8_CR16","doi-asserted-by":"publisher","first-page":"180","DOI":"10.1137\/050622870","volume":"46","author":"C Jansson","year":"2007","unstructured":"Jansson, C., Chaykin, D., Keil, C.: Rigorous error bounds for the optimal value in semidefinite programming. SIAM J. Numer. Anal. 46(1), 180\u2013200 (2007)","journal-title":"SIAM J. Numer. Anal."},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/978-3-319-43425-4_14","volume-title":"Quantitative Evaluation of Systems","author":"BL Kaminski","year":"2016","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C.: Inferring covariances for probabilistic programs. In: Agha, G., Van Houdt, B. (eds.) QEST 2016. LNCS, vol. 9826, pp. 191\u2013206. Springer, Cham (2016). \n                      https:\/\/doi.org\/10.1007\/978-3-319-43425-4_14"},{"key":"8_CR18","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). \n                      https:\/\/doi.org\/10.1007\/978-3-662-49498-1_15"},{"issue":"5","key":"8_CR19","doi-asserted-by":"publisher","first-page":"30:1","DOI":"10.1145\/3208102","volume":"65","author":"BL Kaminski","year":"2018","unstructured":"Kaminski, B.L., Katoen, J.-P., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1\u201330:68 (2018)","journal-title":"J. ACM"},{"key":"8_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-642-15769-1_24","volume-title":"Static Analysis","author":"J-P Katoen","year":"2010","unstructured":"Katoen, J.-P., McIver, A., Meinicke, L., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 390\u2013406. Springer, Heidelberg (2010). \n                      https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24"},{"issue":"3","key":"8_CR21","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."},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"Kura, S., Urabe, N., Hasuo, I.: Tail probabilities for randomized program runtimes via martingales for higher moments. CoRR, abs\/1811.06779 (2018)","DOI":"10.1007\/978-3-030-17465-1_8"},{"key":"8_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"MZ Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M.Z., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). \n                      https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"8_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4","volume-title":"Automated Technology for Verification and Analysis","year":"2018","unstructured":"Lahiri, S.K., Wang, C. (eds.): ATVA 2018. LNCS, vol. 11138. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-030-01090-4"},{"issue":"3","key":"8_CR25","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":"8_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-319-89963-3_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Roux","year":"2018","unstructured":"Roux, P., Iguernlala, M., Conchon, S.: A non-linear arithmetic procedure for control-command software verification. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10806, pp. 132\u2013151. Springer, Cham (2018). \n                      https:\/\/doi.org\/10.1007\/978-3-319-89963-3_8"},{"issue":"2","key":"8_CR27","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/s10703-017-0302-y","volume":"53","author":"P Roux","year":"2018","unstructured":"Roux, P., Voronin, Y.-L., Sankaranarayanan, S.: Validating numerical semidefinite programming solvers for polynomial invariants. Form. Methods Syst. Des. 53(2), 286\u2013312 (2018)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"8_CR28","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/BF01446568","volume":"289","author":"K Schm\u00fcdgen","year":"1991","unstructured":"Schm\u00fcdgen, K.: The k-moment problem for compact semi-algebraic sets. Math. Ann. 289(1), 203\u2013206 (1991)","journal-title":"Math. Ann."},{"key":"8_CR29","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1986","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, New York (1986)"},{"key":"8_CR30","unstructured":"SDPT3. \n                      http:\/\/www.math.nus.edu.sg\/~mattohkc\/SDPT3.html"},{"key":"8_CR31","unstructured":"SOSTOOLS. \n                      http:\/\/sysos.eng.ox.ac.uk\/sostools\/"},{"issue":"7","key":"8_CR32","doi-asserted-by":"publisher","first-page":"901","DOI":"10.1177\/0278364912444146","volume":"31","author":"J Steinhardt","year":"2012","unstructured":"Steinhardt, J., Tedrake, R.: Finite-time regional verification of stochastic non-linear systems. Int. J. Robot. Res. 31(7), 901\u2013923 (2012)","journal-title":"Int. J. Robot. Res."},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Takisaka, T., Oyabu, Y., Urabe, N., Hasuo, I.: Ranking and repulsing supermartingales for reachability in probabilistic programs. In: Lahiri and Wang [24], pp. 476\u2013493","DOI":"10.1007\/978-3-030-01090-4_28"},{"key":"8_CR34","doi-asserted-by":"publisher","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A Tarski","year":"1955","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955)","journal-title":"Pac. J. Math."},{"key":"8_CR35","doi-asserted-by":"crossref","unstructured":"Tolpin, D., van de Meent, J.-W., Yang, H., Wood, F.D.: Design and implementation of probabilistic programming language anglican. In: IFL, pp. 6:1\u20136:12. ACM (2016)","DOI":"10.1145\/3064899.3064910"},{"key":"8_CR36","doi-asserted-by":"crossref","unstructured":"Urabe, N., Hara, M., Hasuo, I.: Categorical liveness checking by corecursive algebras. In: Proceedings of LICS 2017, pp. 1\u201312. IEEE Computer Society (2017)","DOI":"10.1109\/LICS.2017.8005151"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17465-1_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,20]],"date-time":"2019-05-20T09:52:17Z","timestamp":1558345937000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17465-1_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030174644","9783030174651"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17465-1_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"3 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TACAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tacas2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/tacas","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"164","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"42","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"8","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"26% - 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"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"13","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12 full papers and 11 short papers accepted for TOOLympics and SV-COMP (avg. 4 reviewers\/paper, selected from 43 submissions)","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}