{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,11]],"date-time":"2026-05-11T11:20:14Z","timestamp":1778498414660,"version":"3.51.4"},"publisher-location":"Berlin, Heidelberg","reference-count":31,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642157684","type":"print"},{"value":"9783642157691","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-15769-1_24","type":"book-chapter","created":{"date-parts":[[2010,9,13]],"date-time":"2010-09-13T02:09:40Z","timestamp":1284343780000},"page":"390-406","source":"Crossref","is-referenced-by-count":55,"title":["Linear-Invariant Generation for Probabilistic Programs:"],"prefix":"10.1007","author":[{"given":"Joost-Pieter","family":"Katoen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annabelle K.","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Larissa A.","family":"Meinicke","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carroll C.","family":"Morgan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"24_CR1","unstructured":"Probabilistic\u00a0Systems Group, \n                  \n                    http:\/\/www.cse.unsw.edu.au\/~carrollm\/probs"},{"key":"24_CR2","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1016\/B978-044450813-3\/50014-X","volume-title":"Handbook of Automated Reasoning, vol. I","author":"A. Bockmayr","year":"2001","unstructured":"Bockmayr, A., Weispfenning, V.: Solving numerical constraints. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. I, ch.12. vol.\u00a0I, pp. 751\u2013842. Elsevier Science, Amsterdam (2001)"},{"key":"24_CR3","unstructured":"Celiku, O.: Mechanized Reasoning for Dually-Nondeterministic and Probabilistic Programs. PhD thesis, TUCS (2006)"},{"key":"24_CR4","first-page":"131","volume-title":"Quantitative Evaluation of Systems (QEST)","author":"F. Ciesinski","year":"2006","unstructured":"Ciesinski, F., Baier, C.: LiQuor: A tool for qualitative and quantitative linear time analysis of reactive systems. In: Quantitative Evaluation of Systems (QEST), pp. 131\u2013132. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"24_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/978-3-540-45069-6_39","volume-title":"Computer Aided Verification","author":"M. Col\u00f3n","year":"2003","unstructured":"Col\u00f3n, M., Sankaranarayanan, S., Sipma, H.: Linear invariant generation using non-linear constraint solving. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 420\u2013432. Springer, Heidelberg (2003)"},{"key":"24_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/b105073","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Cousot","year":"2005","unstructured":"Cousot, P.: Proving program invariance and termination by parametric abstraction, Lagrangian relaxation and semidefinite programming. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol.\u00a03385, pp. 1\u201324. Springer, Heidelberg (2005)"},{"key":"24_CR7","first-page":"238","volume-title":"Principles of Programming Languages (PoPL)","author":"P. Cousot","year":"1977","unstructured":"Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Principles of Programming Languages (PoPL), pp. 238\u2013252. ACM, New York (1977)"},{"issue":"3","key":"24_CR8","doi-asserted-by":"publisher","first-page":"315","DOI":"10.1142\/S012905410200114X","volume":"13","author":"J. Hartog den","year":"2002","unstructured":"den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a Hoare like logic. Int. J. Found. Comput. Sci.\u00a013(3), 315\u2013340 (2002)","journal-title":"Int. J. Found. Comput. Sci."},{"key":"24_CR9","first-page":"127","volume-title":"Principles and Practice of Declarative Programming (PPDP)","author":"A. Pierro Di","year":"2000","unstructured":"Di Pierro, A., Wiklicky, H.: Concurrent constraint programming: towards probabilistic abstract interpretation. In: Gabbrielli, M., Pfenning, F. (eds.) Principles and Practice of Declarative Programming (PPDP), pp. 127\u2013138. ACM, New York (2000)"},{"key":"24_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1007\/3-540-45142-0_9","volume-title":"Logic Based Program Synthesis and Transformation","author":"A. Pierro Di","year":"2001","unstructured":"Di Pierro, A., Wiklicky, H.: Measuring the precision of abstract interpretations. In: Lau, K. (ed.) LOPSTR 2000. LNCS, vol.\u00a02042, pp. 147\u2013164. Springer, Heidelberg (2001)"},{"key":"24_CR11","volume-title":"A Discipline of Programming","author":"E.W. Dijkstra","year":"1976","unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)"},{"issue":"2","key":"24_CR12","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1145\/261320.261324","volume":"31","author":"A. Dolzmann","year":"1997","unstructured":"Dolzmann, A., Sturm, T.: REDLOG: computer algebra meets computer logic. SIGSAM Bull.\u00a031(2), 2\u20139 (1997)","journal-title":"SIGSAM Bull."},{"key":"24_CR13","series-title":"Proc. Symp. Appl. Math.","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1090\/psapm\/019\/0235771","volume-title":"Mathematical Aspects of Computer Science","author":"R.W. Floyd","year":"1967","unstructured":"Floyd, R.W.: Assigning meanings to programs. In: Schwartz, J.T. (ed.) Mathematical Aspects of Computer Science. Proc. Symp. Appl. Math., vol.\u00a019, pp. 19\u201332. American Mathematical Society, Providence (1967)"},{"issue":"6","key":"24_CR14","first-page":"281","volume":"43","author":"S. Gulwani","year":"2008","unstructured":"Gulwani, S., Srivastava, S., Venkatesan, R.: Program analysis as constraint solving. Programming Language Design and Implementation (PLDI)\u00a043(6), 281\u2013292 (2008)","journal-title":"Programming Language Design and Implementation (PLDI)"},{"key":"24_CR15","volume-title":"Encyclopedia of Mathematics","author":"M. Hazewinkel","year":"2002","unstructured":"Hazewinkel, M.: Encyclopedia of Mathematics. Springer, Heidelberg (2002)"},{"key":"24_CR16","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":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"issue":"10","key":"24_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"C.A.R. Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM\u00a012(10), 576\u2013580 (1969)","journal-title":"Communications of the ACM"},{"key":"24_CR19","unstructured":"Hurd, J.: Formal Verification of Probabilistic Algorithms. PhD thesis, University of Cambridge (2002)"},{"issue":"1","key":"24_CR20","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1016\/j.tcs.2005.08.005","volume":"346","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A.K., Morgan, C.C.: Probabilistic guarded commands mechanised in HOL. Theoretical Computer Science\u00a0346(1), 96\u2013112 (2005)","journal-title":"Theoretical Computer Science"},{"key":"24_CR21","unstructured":"Kapur, D.: Automatically generating loop invariants using quantifier elimination. In: Deduction and Applications (2005)"},{"key":"24_CR22","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., McIver, A.K., Meinicke, L.A., Morgan, C.C.: Linear-invariant generation for probabilistic programs: automated support for proof-based methods. Draft of this paper including its appendices [1, Katoen:10] (2010)","DOI":"10.1007\/978-3-642-15769-1_24"},{"key":"24_CR23","unstructured":"Kattenbelt, M.: Private communication (2010)"},{"key":"24_CR24","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":"24_CR25","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. Jnl. Comp. Sys. Sciences\u00a022, 328\u2013350 (1981)","journal-title":"Jnl. Comp. Sys. Sciences"},{"key":"24_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/978-3-540-78800-3_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Legay","year":"2008","unstructured":"Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 173\u2013187. Springer, Heidelberg (2008)"},{"key":"24_CR27","series-title":"Monographs in Computer Science","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"A.K. McIver","year":"2004","unstructured":"McIver, A.K., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, Heidelberg (2004)"},{"key":"24_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"322","DOI":"10.1007\/978-3-540-45099-3_17","volume-title":"Static Analysis","author":"D. Monniaux","year":"2000","unstructured":"Monniaux, D.: Abstract interpretation of probabilistic semantics. In: Palsberg, J. (ed.) SAS 2000. LNCS, vol.\u00a01824, pp. 322\u2013339. Springer, Heidelberg (2000)"},{"key":"24_CR29","volume-title":"BCS-FACS 7th Refinement Workshop, Workshops in Computing","author":"C.C. Morgan","year":"1996","unstructured":"Morgan, C.C.: Proof rules for probabilistic loops. In: Jifeng, H., Cooke, J., Wallis, P. (eds.) BCS-FACS 7th Refinement Workshop, Workshops in Computing. Springer, Heidelberg (1996)"},{"key":"24_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/978-3-540-24622-0_20","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Podelski","year":"2004","unstructured":"Podelski, A., Rybalchenko, A.: A complete method for the synthesis of linear ranking functions. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol.\u00a02937, pp. 239\u2013251. Springer, Heidelberg (2004)"},{"key":"24_CR31","first-page":"318","volume-title":"Principles of Programming Languages (PoPL)","author":"S. Sankaranarayanan","year":"2004","unstructured":"Sankaranarayanan, S., Sipma, H.B., Manna, Z.: Non-linear loop invariant generation using Gr\u00f6bner bases. In: Principles of Programming Languages (PoPL), pp. 318\u2013329. ACM, New York (2004)"}],"container-title":["Lecture Notes in Computer Science","Static Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-15769-1_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,8]],"date-time":"2020-01-08T21:46:30Z","timestamp":1578519990000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-15769-1_24"}},"subtitle":["Automated Support for Proof-Based Methods"],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642157684","9783642157691"],"references-count":31,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-15769-1_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}