{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T03:46:49Z","timestamp":1772164009348,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":51,"publisher":"ACM","license":[{"start":{"date-parts":[[2016,1,11]],"date-time":"2016-01-11T00:00:00Z","timestamp":1452470400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100002428","name":"Austrian Science Fund","doi-asserted-by":"publisher","award":["P23499-N23, S11407-N23"],"award-info":[{"award-number":["P23499-N23, S11407-N23"]}],"id":[{"id":"10.13039\/501100002428","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001809","name":"National Natural Science Foundation of China","doi-asserted-by":"publisher","award":["61532019"],"award-info":[{"award-number":["61532019"]}],"id":[{"id":"10.13039\/501100001809","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100004963","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["291734"],"award-info":[{"award-number":["291734"]}],"id":[{"id":"10.13039\/501100004963","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2016,1,11]]},"DOI":"10.1145\/2837614.2837639","type":"proceedings-article","created":{"date-parts":[[2016,1,7]],"date-time":"2016-01-07T09:05:00Z","timestamp":1452157500000},"page":"327-342","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":42,"title":["Algorithmic analysis of qualitative and quantitative termination problems for affine probabilistic programs"],"prefix":"10.1145","author":[{"given":"Krishnendu","family":"Chatterjee","sequence":"first","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Hongfei","family":"Fu","sequence":"additional","affiliation":[{"name":"IST Austria, Austria \/ Institute of Software at Chinese Academy of Sciences, China"}]},{"given":"Petr","family":"Novotn\u00fd","sequence":"additional","affiliation":[{"name":"IST Austria, Austria"}]},{"given":"Rouzbeh","family":"Hasheminezhad","sequence":"additional","affiliation":[{"name":"Sharif University of Technology, Iran"}]}],"member":"320","published-online":{"date-parts":[[2016,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"http:\/\/www- 01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/","author":"Optimizer IBM ILOG CPLEX","year":"2010","unstructured":"IBM ILOG CPLEX Optimizer . http:\/\/www- 01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/ , 2010 . IBM ILOG CPLEX Optimizer. http:\/\/www- 01.ibm.com\/software\/integration\/optimization\/cplex-optimizer\/, 2010."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.2748\/tmj\/1178243286"},{"key":"e_1_3_2_1_3_1","volume-title":"Principles of model checking","author":"Baier C.","year":"2008","unstructured":"C. Baier and J.-P. Katoen . Principles of model checking . MIT Press , 2008 . ISBN 978-0-262-02649-9. C. Baier and J.-P. Katoen. Principles of model checking. MIT Press, 2008. ISBN 978-0-262-02649-9."},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1962.10482149"},{"key":"e_1_3_2_1_5_1","volume-title":"Probability and Measure","author":"Billingsley P.","year":"1995","unstructured":"P. Billingsley . Probability and Measure . Wiley , 3 rd edition, 1995 . P. Billingsley. Probability and Measure. Wiley, 3rd edition, 1995.","edition":"3"},{"key":"e_1_3_2_1_6_1","first-page":"50813","volume-title":"Elsevier and MIT Press","author":"Bockmayr A.","year":"2001","unstructured":"A. Bockmayr and V. Weispfenning . Solving numerical constraints. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 751\u2013842 . Elsevier and MIT Press , 2001 . ISBN 0-444- 50813 - 50819 . A. Bockmayr and V. Weispfenning. Solving numerical constraints. In J. A. Robinson and A. Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes), pages 751\u2013842. Elsevier and MIT Press, 2001. ISBN 0-444-50813-9."},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-32033-3_24"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_109"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_48"},{"key":"e_1_3_2_1_10_1","unstructured":"ISBN 3-540-27231-3..  ISBN 3-540-27231-3.."},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0166-0"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/62212.62257"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2958031.2958114"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837639"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1080\/15427951.2006.10129115"},{"key":"e_1_3_2_1_16_1","volume-title":"7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings","volume":"2031","author":"Col\u00f3n M.","year":"2001","unstructured":"M. Col\u00f3n and H. Sipma . Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems , 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings , volume 2031 of Lecture Notes in Computer Science, pages 67\u201381. Springer , 2001 . ISBN 3-540-41865-2.. M. Col\u00f3n and H. Sipma. Synthesis of linear ranking functions. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2031 of Lecture Notes in Computer Science, pages 67\u201381. Springer, 2001. ISBN 3-540-41865-2.."},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_4"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511581274","volume-title":"Concentration of Measure for the Analysis of Randomized Algorithms","author":"Dubhashi D.","year":"2009","unstructured":"D. Dubhashi and A. Panconesi . Concentration of Measure for the Analysis of Randomized Algorithms . Cambridge University Press , New York, NY, USA , 1 st edition, 2009 . ISBN 0521884276, 9780521884273. D. Dubhashi and A. Panconesi. Concentration of Measure for the Analysis of Randomized Algorithms. Cambridge University Press, New York, NY, USA, 1st edition, 2009. ISBN 0521884276, 9780521884273.","edition":"1"},{"key":"e_1_3_2_1_20_1","volume-title":"Probability: Theory and Examples","author":"Durrett R.","year":"1996","unstructured":"R. Durrett . Probability: Theory and Examples ( Second Edition). Duxbury Press , 1996 . R. Durrett. Probability: Theory and Examples (Second Edition). Duxbury Press, 1996."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2005.39"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_14"},{"key":"e_1_3_2_1_23_1","first-page":"457","article-title":"A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian)","volume":"12","author":"Farkas J.","year":"1894","unstructured":"J. Farkas . A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian) . Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6 , 12 : 457 \u2013 472 , 1894 . J. Farkas. A fourier-f\u00e9le mechanikai elv alkalmaz\u00e1sai (Hungarian). Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6, 12:457\u2013472, 1894.","journal-title":"Mathematikai\u00e9s Term\u00e9szettudom\u00e1nyi \u00c9rtesit\u00f6"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677001"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177728976"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1137\/0214070"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1963.10500830"},{"key":"e_1_3_2_1_29_1","volume-title":"Dynamic Programming and Markov Processes","author":"Howard H.","year":"1960","unstructured":"H. Howard . Dynamic Programming and Markov Processes . MIT Press , 1960 . H. Howard. Dynamic Programming and Markov Processes. MIT Press, 1960."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5555\/1622737.1622748"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(98)00023-X"},{"key":"e_1_3_2_1_32_1","first-page":"406","volume-title":"SAS","author":"Katoen J.","year":"2010","unstructured":"J. Katoen , A. McIver , L. Meinicke , and C. C. Morgan . Linear-invariant generation for probabilistic programs: - automated support for proofbased methods . In SAS , volume LNCS 6337 , Springer , pages 390\u2013 406 , 2010 . J. Katoen, A. McIver, L. Meinicke, and C. C. Morgan. Linear-invariant generation for probabilistic programs: - automated support for proofbased methods. In SAS, volume LNCS 6337, Springer, pages 390\u2013406, 2010."},{"key":"e_1_3_2_1_33_1","volume-title":"Denumerable Markov Chains","author":"Kemeny J.","year":"1966","unstructured":"J. Kemeny , J. Snell , and A. Knapp . Denumerable Markov Chains . D. Van Nostrand Company , 1966 . J. Kemeny, J. Snell, and A. Knapp. Denumerable Markov Chains. D. Van Nostrand Company, 1966."},{"key":"e_1_3_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/TRO.2009.2030225"},{"key":"e_1_3_2_1_35_1","first-page":"591","volume-title":"CAV, LNCS 6806","author":"Kwiatkowska M. Z.","year":"2011","unstructured":"M. Z. Kwiatkowska , G. Norman , and D. Parker . Prism 4.0: Verification of probabilistic real-time systems . In CAV, LNCS 6806 , pages 585\u2013 591 , 2011 . M. Z. Kwiatkowska, G. Norman, and D. Parker. Prism 4.0: Verification of probabilistic real-time systems. In CAV, LNCS 6806, pages 585\u2013591, 2011."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.360210"},{"key":"e_1_3_2_1_37_1","first-page":"248","volume-title":"Probabilistic Methods for Algorithmic Discrete Mathematics","author":"McDiarmid C.","unstructured":"C. McDiarmid . Concentration . In Probabilistic Methods for Algorithmic Discrete Mathematics , pages 195\u2013 248 . 1998. C. McDiarmid. Concentration. In Probabilistic Methods for Algorithmic Discrete Mathematics, pages 195\u2013248. 1998."},{"key":"e_1_3_2_1_38_1","first-page":"155","volume-title":"PSSE","author":"McIver A.","year":"2004","unstructured":"A. McIver and C. Morgan . Developing and reasoning about probabilistic programs in pGCL . In PSSE , pages 123\u2013 155 , 2004 . A. McIver and C. Morgan. Developing and reasoning about probabilistic programs in pGCL. In PSSE, pages 123\u2013155, 2004."},{"key":"e_1_3_2_1_39_1","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science","author":"McIver A.","year":"2005","unstructured":"A. McIver and C. Morgan . Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science . Springer , 2005 . A. McIver and C. Morgan. Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, 2005."},{"key":"e_1_3_2_1_40_1","volume-title":"8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings","volume":"2126","author":"Monniaux D.","year":"2001","unstructured":"D. Monniaux . An abstract analysis of the probabilistic termination of programs. In P. Cousot, editor, Static Analysis , 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings , volume 2126 of Lecture Notes in Computer Science, pages 111\u2013126. Springer , 2001 . ISBN 3-540-42314-1.. URL http:\/\/dx.doi. org\/10.1007\/3-540-47764-0_7. D. Monniaux. An abstract analysis of the probabilistic termination of programs. In P. Cousot, editor, Static Analysis, 8th International Symposium, SAS 2001, Paris, France, July 16-18, 2001, Proceedings, volume 2126 of Lecture Notes in Computer Science, pages 111\u2013126. Springer, 2001. ISBN 3-540-42314-1.. URL http:\/\/dx.doi. org\/10.1007\/3-540-47764-0_7."},{"key":"e_1_3_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/211390"},{"key":"e_1_3_2_1_43_1","volume-title":"Introduction to probabilistic automata (Computer science and applied mathematics)","author":"Paz A.","year":"1971","unstructured":"A. Paz . Introduction to probabilistic automata (Computer science and applied mathematics) . Academic Press , 1971 . A. Paz. Introduction to probabilistic automata (Computer science and applied mathematics). Academic Press, 1971."},{"key":"e_1_3_2_1_44_1","unstructured":"A.\n      Podelski\n     and \n      A.\n      Rybalchenko\n  . \n  A complete method for the synthesis of linear ranking functions\n  . In B. Steffen and G. Levi editors Verification Model Checking and Abstract Interpretation 5th International Conference VMCAI \n  2004 Venice January 11-13 2004 Proceedings volume \n  2937\n   of \n  Lecture Notes in Computer Science pages 239\u2013\n  251\n  . Springer 2004. ISBN 3-540-20803-8..  A. Podelski and A. Rybalchenko. A complete method for the synthesis of linear ranking functions. In B. Steffen and G. Levi editors Verification Model Checking and Abstract Interpretation 5th International Conference VMCAI 2004 Venice January 11-13 2004 Proceedings volume 2937 of Lecture Notes in Computer Science pages 239\u2013251. Springer 2004. ISBN 3-540-20803-8.."},{"key":"e_1_3_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(63)90290-0"},{"key":"e_1_3_2_1_46_1","volume-title":"World Scientific Publishing Company","author":"Rosenthal J. S.","year":"2006","unstructured":"J. S. Rosenthal . A First Look at Rigorous Probability Theory . World Scientific Publishing Company , 2 nd edition, 2006 . J. S. Rosenthal. A First Look at Rigorous Probability Theory. World Scientific Publishing Company, 2nd edition, 2006.","edition":"2"},{"key":"e_1_3_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462179"},{"key":"e_1_3_2_1_48_1","volume-title":"Combinatorial Optimization - Polyhedra and Efficiency","author":"Schrijver A.","year":"2003","unstructured":"A. Schrijver . Combinatorial Optimization - Polyhedra and Efficiency . Springer , 2003 . ISBN 978-3-540-44389-6. A. Schrijver. Combinatorial Optimization - Polyhedra and Efficiency. Springer, 2003. ISBN 978-3-540-44389-6."},{"key":"e_1_3_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1137\/0213021"},{"key":"e_1_3_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/113413.113433"},{"key":"e_1_3_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065010.1065045"},{"key":"e_1_3_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511813658"}],"event":{"name":"POPL '16: The 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"St. Petersburg FL USA","acronym":"POPL '16","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837639","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2837614.2837639","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T01:43:37Z","timestamp":1750211017000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2837614.2837639"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,11]]},"references-count":51,"alternative-id":["10.1145\/2837614.2837639","10.1145\/2837614"],"URL":"https:\/\/doi.org\/10.1145\/2837614.2837639","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/2914770.2837639","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2016,1,11]]},"assertion":[{"value":"2016-01-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}