{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T05:41:12Z","timestamp":1725514872756},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540682356"},{"type":"electronic","value":"9783540682370"}],"license":[{"start":{"date-parts":[[2008,1,1]],"date-time":"2008-01-01T00:00:00Z","timestamp":1199145600000},"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":[[2008]]},"DOI":"10.1007\/978-3-540-68237-0_9","type":"book-chapter","created":{"date-parts":[[2008,6,4]],"date-time":"2008-06-04T01:36:00Z","timestamp":1212543360000},"page":"100-115","source":"Crossref","is-referenced-by-count":3,"title":["Proofs and Refutations for Probabilistic Refinement"],"prefix":"10.1007","author":[{"given":"A. K.","family":"McIver","sequence":"first","affiliation":[]},{"given":"C. C.","family":"Morgan","sequence":"additional","affiliation":[]},{"given":"C.","family":"Gonzalia","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"9_CR1","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"R.-J.R. Back","year":"1998","unstructured":"Back, R.-J.R., von Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)"},{"issue":"5","key":"9_CR2","doi-asserted-by":"publisher","first-page":"752","DOI":"10.1145\/876638.876643","volume":"50","author":"E. Clarke","year":"2003","unstructured":"Clarke, E., Lu, Y., Grumberg, O., Jha, S., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. Journal of the ACM\u00a050(5), 752\u2013794 (2003)","journal-title":"Journal of the ACM"},{"key":"9_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/10722010_4","volume-title":"Mathematics of Program Construction","author":"E. Cohen","year":"2000","unstructured":"Cohen, E.: Separation and reduction. In: Backhouse, R., Oliveira, J.N. (eds.) MPC 2000. LNCS, vol.\u00a01837, pp. 45\u201359. Springer, Heidelberg (2000)"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/978-3-540-71316-6_25","volume-title":"Programming Languages and Systems","author":"Y. Deng","year":"2007","unstructured":"Deng, Y., van Glabeek, R., Morgan, C.C., Zhang, C.: Scalar Outcomes Suffice for Finitary Probabilistic Testing. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol.\u00a04421, pp. 363\u2013378. Springer, Heidelberg (2007)"},{"key":"9_CR5","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)"},{"key":"9_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"212","DOI":"10.1007\/978-3-540-76650-6_13","volume-title":"Formal Methods and Software Engineering","author":"C. Gonzalia","year":"2007","unstructured":"Gonzalia, C., McIver, A.K.: Automating Refinement Checking in Probabilistic System Design. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol.\u00a04789, pp. 212\u2013231. Springer, Heidelberg (2007)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"72","DOI":"10.1007\/978-3-540-71209-1_8","volume-title":"Compiler Construction","author":"T. Han","year":"2007","unstructured":"Han, T., Katoen, J.-P.: Counterexamples in probabilistic model checking. In: Krishnamurthi, S., Odersky, M. (eds.) CC 2007. LNCS, vol.\u00a04420, pp. 72\u201386. Springer, Heidelberg (2007)"},{"key":"9_CR9","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"J. He","year":"1997","unstructured":"He, J., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Science of Computer Programming\u00a028, 171\u2013192 (1997)","journal-title":"Science of Computer Programming"},{"key":"9_CR10","series-title":"ENTCS","volume-title":"Proc 4th QAPL","author":"J. Hurd","year":"2005","unstructured":"Hurd, J., McIver, A.K., Morgan, C.C.: Probabilistic guarded commands mechanised in HOL. In: Cerone, A., de Pierro, A. (eds.) Proc 4th QAPL. ENTCS, vol.\u00a0112, Elsevier, Amsterdam (2005)"},{"issue":"2","key":"9_CR11","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1016\/0022-0000(85)90012-1","volume":"30","author":"D. Kozen","year":"1985","unstructured":"Kozen, D.: A probabilistic PDL. Jnl. Comp. Sys. Sci.\u00a030(2), 162\u2013178 (1985)","journal-title":"Jnl. Comp. Sys. Sci."},{"key":"9_CR12","volume-title":"Tech. Mono. Comp. Sci.","author":"A.K. McIver","year":"2005","unstructured":"McIver, A.K., Morgan, C.C.: Abstraction, Refinement and Proof for Probabilistic Systems. In: Tech. Mono. Comp. Sci., Springer, New York (2005)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"McIver, A.K., Morgan, C.C., Gonzalia, C.: Proofs and refutations for probabilistic systems (2007), http:\/\/www.ics.mq.edu.au\/~anabel\/FM08.pdf","DOI":"10.1007\/978-3-540-68237-0_9"},{"key":"9_CR14","volume-title":"Programming from Specifications","author":"C.C. Morgan","year":"1994","unstructured":"Morgan, C.C.: Programming from Specifications, 2nd edn. Prentice-Hall, Englewood Cliffs (1994)","edition":"2"},{"issue":"3","key":"9_CR15","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C.C. Morgan","year":"1996","unstructured":"Morgan, C.C., McIver, A.K., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Prog. Lang. Sys.\u00a018(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Prog. Lang. Sys."},{"key":"9_CR16","volume-title":"Theory of Games and Economic Behavior","author":"J. Neumann von","year":"1947","unstructured":"von Neumann, J., Morgenstern, O.: Theory of Games and Economic Behavior, 2nd edn. Princeton University Press, Princeton (1947)","edition":"2"}],"container-title":["Lecture Notes in Computer Science","FM 2008: Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-68237-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,18]],"date-time":"2023-05-18T13:01:05Z","timestamp":1684414865000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-68237-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540682356","9783540682370"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-68237-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}