{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T20:08:42Z","timestamp":1774987722279,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642401954","type":"print"},{"value":"9783642401961","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40196-1_17","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:54:56Z","timestamp":1374544496000},"page":"193-208","source":"Crossref","is-referenced-by-count":27,"title":["Prinsys\u2014On a Quest for Probabilistic Loop Invariants"],"prefix":"10.1007","author":[{"given":"Friedrich","family":"Gretz","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Annabelle","family":"McIver","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-31113-0_1","volume-title":"Mathematics of Program Construction","author":"G. Barthe","year":"2012","unstructured":"Barthe, G., Gr\u00e9goire, B., B\u00e9guelin, S.Z.: Probabilistic relational Hoare logics for computer-aided security proofs. In: Gibbons, J., Nogueira, P. (eds.) MPC 2012. LNCS, vol.\u00a07342, pp. 1\u20136. Springer, Heidelberg (2012)"},{"key":"17_CR2","doi-asserted-by":"crossref","unstructured":"Barthe, G., K\u00f6pf, B., Olmedo, F., B\u00e9guelin, S.Z.: Probabilistic relational reasoning for differential privacy. In: Symp. on Principles of Programming Languages (POPL), pp. 97\u2013110. ACM (2012)","DOI":"10.1145\/2103621.2103670"},{"key":"17_CR3","unstructured":"Gretz, F.: Invariant Generation for Linear Probabilistic Programs. Master\u2019s thesis, RWTH Aachen (2010), \n                    \n                      http:\/\/www-i2.informatik.rwth-aachen.de\/i2\/gretz\/"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Gretz, F., Katoen, J.P., McIver, A.: Operational versus Weakest Precondition Semantics for the Probabilistic Guarded Command Language. In: QEST, pp. 168\u2013177 (2012)","DOI":"10.1109\/QEST.2012.21"},{"key":"17_CR5","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)"},{"issue":"1","key":"17_CR6","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E.M. Hahn","year":"2011","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic Reachability for Parametric Markov Models. STTT\u00a013(1), 3\u201319 (2011)","journal-title":"STTT"},{"key":"17_CR7","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.K., Meinicke, L.A., Morgan, C.C.: Linear-Invariant Generation for Probabilistic Programs: In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol.\u00a06337, pp. 390\u2013406. Springer, Heidelberg (2010)"},{"key":"17_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-642-28729-9_31","volume-title":"Foundations of Software Science and Computational Structures","author":"S. Kiefer","year":"2012","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: On the Complexity of the Equivalence Problem for Probabilistic Automata. In: Birkedal, L. (ed.) FOSSACS 2012. LNCS, vol.\u00a07213, pp. 467\u2013481. Springer, Heidelberg (2012)"},{"key":"17_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/978-3-642-31424-7_51","volume-title":"Computer Aided Verification","author":"S. Kiefer","year":"2012","unstructured":"Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J.: APEX: An Analyzer for Open Probabilistic Programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 693\u2013698. Springer, Heidelberg (2012)"},{"key":"17_CR10","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":"M. Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: Verification of Probabilistic Real-time Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol.\u00a06806, pp. 585\u2013591. Springer, Heidelberg (2011)"},{"key":"17_CR11","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof For Probabilistic Systems. Monographs in Computer Science. Springer (2004)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Sankaranarayanan, S., Sipma, H., Manna, Z.: Non-linear Loop Invariant Generation Using Gr\u00f6bner Bases. In: POPL, pp. 318\u2013329 (2004)","DOI":"10.1145\/982962.964028"},{"issue":"6","key":"17_CR13","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1145\/2049706.2049708","volume":"33","author":"M. Ying","year":"2011","unstructured":"Ying, M.: Floyd-Hoare logic for quantum programs. ACM Trans. Program. Lang. Syst.\u00a033(6), 19 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."}],"container-title":["Lecture Notes in Computer Science","Quantitative Evaluation of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40196-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,16]],"date-time":"2019-05-16T02:42:56Z","timestamp":1557974576000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-40196-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401954","9783642401961"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40196-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}