{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:21:54Z","timestamp":1770283314595,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642314230","type":"print"},{"value":"9783642314247","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31424-7_14","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T14:26:49Z","timestamp":1340288809000},"page":"123-138","source":"Crossref","is-referenced-by-count":39,"title":["Proving Termination of Probabilistic Programs Using Patterns"],"prefix":"10.1007","author":[{"given":"Javier","family":"Esparza","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andreas","family":"Gaiser","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Stefan","family":"Kiefer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/3-540-36576-1_6","volume-title":"Foundations of Software Science and Computational Structures","author":"T. Arons","year":"2003","unstructured":"Arons, T., Pnueli, A., Zuck, L.D.: Parameterized Verification by Probabilistic Abstraction. In: Gordon, A.D. (ed.) FOSSACS 2003. LNCS, vol.\u00a02620, pp. 87\u2013102. Springer, Heidelberg (2003)"},{"key":"14_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of model checking. MIT Press (2008)"},{"key":"14_CR3","doi-asserted-by":"publisher","first-page":"824","DOI":"10.1145\/4221.214134","volume":"32","author":"G. Bracha","year":"1985","unstructured":"Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM\u00a032, 824\u2013840 (1985)","journal-title":"J. ACM"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"415","DOI":"10.1007\/11817963_37","volume-title":"Computer Aided Verification","author":"B. Cook","year":"2006","unstructured":"Cook, B., Podelski, A., Rybalchenko, A.: Terminator: Beyond Safety. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 415\u2013418. Springer, Heidelberg (2006)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-642-23702-7_25","volume-title":"Static Analysis","author":"J. Esparza","year":"2011","unstructured":"Esparza, J., Gaiser, A.: Probabilistic Abstractions with Arbitrary Domains. In: Yahav, E. (ed.) SAS 2011. LNCS, vol.\u00a06887, pp. 334\u2013350. Springer, Heidelberg (2011)"},{"key":"14_CR6","unstructured":"Esparza, J., Gaiser, A., Kiefer, S.: Proving termination of probabilistic programs using patterns. Technical report (2012), \n                    \n                      http:\/\/arxiv.org\/abs\/1204.2932"},{"key":"14_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/978-3-642-12002-2_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"E.M. Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PASS: Abstraction Refinement for Infinite Probabilistic Models. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 353\u2013357. Springer, Heidelberg (2010)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-70545-1_16","volume-title":"Computer Aided Verification","author":"H. Hermanns","year":"2008","unstructured":"Hermanns, H., Wachter, B., Zhang, L.: Probabilistic CEGAR. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 162\u2013175. Springer, Heidelberg (2008)"},{"key":"14_CR9","unstructured":"Holzmann, G.: The Spin Model Checker: Primer and Reference Manual, 1st edn. Addison-Wesley Professional (2003)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-540-93900-9_17","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"M. Kattenbelt","year":"2009","unstructured":"Kattenbelt, M., Kwiatkowska, M., Norman, G., Parker, D.: Abstraction Refinement for Probabilistic Software. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 182\u2013197. Springer, Heidelberg (2009)"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/11889229_4","volume-title":"Refinement Techniques in Software Engineering","author":"A. McIver","year":"2006","unstructured":"McIver, A., Morgan, C.: Developing and Reasoning About Probabilistic Programs in pGCL. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol.\u00a03167, pp. 123\u2013155. Springer, Heidelberg (2006)"},{"key":"14_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/3-540-44880-2_15","volume-title":"ZB 2003: Formal Specification and Development in Z and B","author":"A. McIver","year":"2003","unstructured":"McIver, A., Morgan, C., Hoang, T.S.: Probabilistic Termination in B. In: Bert, D., Bowen, J. P., King, S., Wald\u00e9n, M. (eds.) ZB 2003. LNCS, vol.\u00a02651, pp. 216\u2013239. Springer, Heidelberg (2003)"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1007\/3-540-47764-0_7","volume-title":"Static Analysis","author":"D. Monniaux","year":"2001","unstructured":"Monniaux, D.: An Abstract Analysis of the Probabilistic Termination of Programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol.\u00a02126, pp. 111\u2013126. Springer, Heidelberg (2001)"},{"issue":"3","key":"14_CR14","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1016\/j.tcs.2005.05.022","volume":"349","author":"T. Nakata","year":"2005","unstructured":"Nakata, T.: On the expected time for Herman\u2019s probabilistic self-stabilizing algorithm. Theoretical Computer Science\u00a0349(3), 475\u2013483 (2005)","journal-title":"Theoretical Computer Science"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: On the extremely fair treatment of probabilistic algorithms. In: STOC, pp. 278\u2013290. ACM (1983)","DOI":"10.1145\/800061.808757"},{"key":"14_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1993.1012","volume":"103","author":"A. Pnueli","year":"1993","unstructured":"Pnueli, A., Zuck, L.D.: Probabilistic verification. Inf. Comput.\u00a0103, 1\u201329 (1993)","journal-title":"Inf. Comput."},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Podelski, A., Rybalchenko, A.: Transition invariants. In: LICS, pp. 32\u201341. IEEE Computer Society (2004)","DOI":"10.1109\/LICS.2004.1319598"},{"key":"14_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/978-3-540-69611-7_16","volume-title":"Practical Aspects of Declarative Languages","author":"A. Podelski","year":"2006","unstructured":"Podelski, A., Rybalchenko, A.: ARMC: The Logical Choice for Software Model Checking with Abstraction Refinement. In: Hanus, M. (ed.) PADL 2007. LNCS, vol.\u00a04354, pp. 245\u2013259. Springer, Heidelberg (2006)"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-642-19835-9_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Podelski","year":"2011","unstructured":"Podelski, A., Rybalchenko, A.: Transition Invariants and Transition Predicate Abstraction for Program Termination. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol.\u00a06605, pp. 3\u201310. Springer, Heidelberg (2011)"},{"key":"14_CR20","unstructured":"Rybalchenko, A.: Temporal verification with transition invariants. PhD thesis (2005)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31424-7_14.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T11:59:46Z","timestamp":1620129586000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31424-7_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642314230","9783642314247"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31424-7_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012]]}}}