{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,1]],"date-time":"2025-10-01T16:31:29Z","timestamp":1759336289371,"version":"3.40.3"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030294359"},{"type":"electronic","value":"9783030294366"}],"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-29436-6_16","type":"book-chapter","created":{"date-parts":[[2019,8,20]],"date-time":"2019-08-20T16:04:02Z","timestamp":1566317042000},"page":"269-286","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":14,"title":["Computing Expected Runtimes for Constant Probability Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0283-8520","authenticated-orcid":false,"given":"J\u00fcrgen","family":"Giesl","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1421-6980","authenticated-orcid":false,"given":"Peter","family":"Giesl","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5111-3177","authenticated-orcid":false,"given":"Marcel","family":"Hark","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,8,20]]},"reference":[{"key":"16_CR1","doi-asserted-by":"publisher","first-page":"34:1","DOI":"10.1145\/3158122","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. Proc. ACM Program. Lang. (POPL) 2, 34:1\u201334:32 (2018). https:\/\/doi.org\/10.1145\/3158122","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"16_CR2","unstructured":"Ash, R.B., Doleans-Dade, C.A.: Probability and Measure Theory. Elsevier\/Academic Press (2000)"},{"issue":"1","key":"16_CR3","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.: The solution of linear probabilistic recurrence relations. Algorithmica 36(1), 41\u201357 (2003). https:\/\/doi.org\/10.1007\/s00453-002-1003-4","journal-title":"Algorithmica"},{"key":"16_CR4","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":"16_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/11817963_34","volume-title":"Computer Aided Verification","author":"M Braverman","year":"2006","unstructured":"Braverman, M.: Termination of integer linear programs. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 372\u2013385. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_34"},{"key":"16_CR6","doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Brozek, V., Etessami, K.: One-counter stochastic games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2010, LIPIcs, vol. 8, pp. 108\u2013119 (2010). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2010.108","DOI":"10.4230\/LIPIcs.FSTTCS.2010.108"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-642-31585-5_16","volume-title":"Automata, Languages, and Programming","author":"T Br\u00e1zdil","year":"2012","unstructured":"Br\u00e1zdil, T., Ku\u010dera, A., Novotn\u00fd, P., Wojtczak, D.: Minimizing expected termination time in one-counter Markov decision processes. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012. LNCS, vol. 7392, pp. 141\u2013152. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31585-5_16"},{"issue":"2","key":"16_CR8","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/s10703-012-0166-0","volume":"43","author":"T Br\u00e1zdil","year":"2013","unstructured":"Br\u00e1zdil, T., Esparza, J., Kiefer, S., Kucera, A.: Analyzing probabilistic pushdown automata. Formal Methods Syst. Des. 43(2), 124\u2013163 (2013). https:\/\/doi.org\/10.1007\/s10703-012-0166-0","journal-title":"Formal Methods Syst. Des."},{"issue":"4","key":"16_CR9","doi-asserted-by":"publisher","first-page":"13:1","DOI":"10.1145\/2866575","volume":"38","author":"M Brockschmidt","year":"2016","unstructured":"Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Analyzing runtime and size complexity of integer programs. ACM Trans. Program. Lang. Syst. 38(4), 13:1\u201313:50 (2016). https:\/\/doi.org\/10.1145\/2866575","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR10","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":"16_CR11","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":"16_CR12","doi-asserted-by":"publisher","unstructured":"Chatterjee, K., Novotn\u00fd, P., Zikelic, D.: Stochastic invariants for probabilistic termination. In: Castagna, G., Gordon, A.D. (eds.) POPL 2017, pp. 145\u2013160 (2017). https:\/\/doi.org\/10.1145\/3093333.3009873","DOI":"10.1145\/3093333.3009873"},{"issue":"2","key":"16_CR13","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). https:\/\/doi.org\/10.1145\/3174800","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"16_CR14","doi-asserted-by":"publisher","DOI":"10.1007\/0-387-27602-5","volume-title":"An Introduction to Difference Equations","author":"S Elaydi","year":"2005","unstructured":"Elaydi, S.: An Introduction to Difference Equations. Springer, New York (2005). https:\/\/doi.org\/10.1007\/0-387-27602-5"},{"key":"16_CR15","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kucera, A., Mayr, R.: Quantitative analysis of probabilistic pushdown automata: expectations and variances. In: Panangaden, P. (ed.) LICS 2005, pp. 117\u2013126 (2005). https:\/\/doi.org\/10.1109\/LICS.2005.39","DOI":"10.1109\/LICS.2005.39"},{"key":"16_CR16","volume-title":"An Introduction to Probability Theory and Its Applications, Probability and Mathematical Statistics","author":"W Feller","year":"1950","unstructured":"Feller, W.: An Introduction to Probability Theory and Its Applications, Probability and Mathematical Statistics, vol. 1. Wiley, Hoboken (1950)"},{"key":"16_CR17","doi-asserted-by":"publisher","unstructured":"Fioriti, L.M.F., Hermanns, H.: Probabilistic termination: soundness, completeness, and compositionality. In: Rajamani, S.K., Walker, D. (eds.) POPL 2015, pp. 489\u2013501 (2015). https:\/\/doi.org\/10.1145\/2676726.2677001","DOI":"10.1145\/2676726.2677001"},{"key":"16_CR18","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-030-25543-5_24","volume-title":"Proceedings of CAV 2019","author":"F Frohn","year":"2019","unstructured":"Frohn, F., Giesl, J.: Termination of triangular integer loops is decidable. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11562, pp. 426\u2013444. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_24"},{"key":"16_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"468","DOI":"10.1007\/978-3-030-11245-5_22","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"H Fu","year":"2019","unstructured":"Fu, H., Chatterjee, K.: Termination of nondeterministic probabilistic programs. In: Enea, C., Piskac, R. (eds.) VMCAI 2019. LNCS, vol. 11388, pp. 468\u2013490. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-11245-5_22"},{"key":"16_CR20","doi-asserted-by":"crossref","unstructured":"Giesl, J., Giesl, P., Hark, M.: Computing expected runtimes for constant probability programs. CoRR abs\/1905.09544 (2019). https:\/\/arxiv.org\/abs\/1905.09544","DOI":"10.1007\/978-3-030-29436-6_16"},{"key":"16_CR21","doi-asserted-by":"crossref","DOI":"10.1093\/oso\/9780198572237.001.0001","volume-title":"Probability and Random Processes","author":"G Grimmett","year":"2001","unstructured":"Grimmett, G., Stirzaker, D.: Probability and Random Processes. Oxford University Press, Oxford (2001)"},{"key":"16_CR22","unstructured":"Johansson, F., et al.: MpMath: a Python library for arbitrary-precision floating-point arithmetic. http:\/\/mpmath.org\/"},{"key":"16_CR23","doi-asserted-by":"publisher","unstructured":"Kaminski, B.L., Katoen, J.: On the hardness of almost-sure termination. In: Italiano, G.F., Pighizzini, G., Sannella, D. (eds.) MFCS 2015. LNCS, vol. 9234, pp. 307\u2013318. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-48057-1_24","DOI":"10.1007\/978-3-662-48057-1_24"},{"key":"16_CR24","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":"16_CR25","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":"16_CR26","doi-asserted-by":"publisher","unstructured":"Kozen, D.: Semantics of probabilistic programs. In: Kosaraju, S.R. (ed.) FOCS 1979, pp. 101\u2013114 (1979). https:\/\/doi.org\/10.1109\/SFCS.1979.38","DOI":"10.1109\/SFCS.1979.38"},{"key":"16_CR27","doi-asserted-by":"publisher","DOI":"10.1007\/b138392","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A McIver","year":"2005","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392"},{"key":"16_CR28","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/3158121","volume":"2","author":"A McIver","year":"2018","unstructured":"McIver, A., Morgan, C., Kaminski, B.L., Katoen, J.: A new proof rule for almost-sure termination. Proc. ACM Program. Lang. (POPL) 2, 33:1\u201333:28 (2018). https:\/\/doi.org\/10.1145\/3158121","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"16_CR29","doi-asserted-by":"publisher","first-page":"e103","DOI":"10.7717\/peerj-cs.103","volume":"3","author":"A Meurer","year":"2017","unstructured":"Meurer, A., et al.: SymPy: symbolic computing in Python. Peer J Comput. Sci. 3, e103 (2017). https:\/\/doi.org\/10.7717\/peerj-cs.103","journal-title":"Peer J Comput. Sci."},{"key":"16_CR30","doi-asserted-by":"publisher","unstructured":"Ngo, V.C., Carbonneaux, Q., Hoffmann, J.: Bounded expectations: resource analysis for probabilistic programs. In: Foster, J.S., Grossman, D. (eds.) PLDI 2018, pp. 496\u2013512 (2018). https:\/\/doi.org\/10.1145\/3192366.3192394. Extended Version available at https:\/\/arxiv.org\/abs\/1711.08847","DOI":"10.1145\/3192366.3192394"},{"key":"16_CR31","doi-asserted-by":"publisher","unstructured":"Ouaknine, J., Pinto, J.S., Worrell, J.: On termination of integer linear loops. In: Indyk, P. (ed.) SODA 2015, pp. 957\u2013969 (2015). https:\/\/doi.org\/10.1137\/1.9781611973730.65","DOI":"10.1137\/1.9781611973730.65"},{"key":"16_CR32","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"ML Puterman","year":"1994","unstructured":"Puterman, M.L.: Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York (1994)"},{"key":"16_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4229-9","volume-title":"Principles of Random Walk","author":"F Spitzer","year":"1964","unstructured":"Spitzer, F.: Principles of Random Walk. Springer, New York (1964). https:\/\/doi.org\/10.1007\/978-1-4757-4229-9"},{"key":"16_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"560","DOI":"10.1007\/978-3-319-94821-8_33","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.) ITP 2018. LNCS, vol. 10895, pp. 560\u2013578. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94821-8_33"},{"key":"16_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-540-27813-9_6","volume-title":"Computer Aided Verification","author":"A Tiwari","year":"2004","unstructured":"Tiwari, A.: Termination of linear programs. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 70\u201382. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_6"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 27"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29436-6_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T07:10:00Z","timestamp":1721632200000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-29436-6_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030294359","9783030294366"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29436-6_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"20 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Natal","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Brazil","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":"27 August 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 August 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.mat.ufrn.br\/CADE-27\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}