{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,10]],"date-time":"2026-02-10T20:15:38Z","timestamp":1770754538677,"version":"3.50.0"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030887001","type":"print"},{"value":"9783030887018","type":"electronic"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-88701-8_28","type":"book-chapter","created":{"date-parts":[[2021,10,21]],"date-time":"2021-10-21T23:06:25Z","timestamp":1634857585000},"page":"465-482","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":7,"title":["Automated Reasoning for Probabilistic Sequential Programs with Theorem Proving"],"prefix":"10.1007","author":[{"given":"Kangfeng","family":"Ye","sequence":"first","affiliation":[]},{"given":"Simon","family":"Foster","sequence":"additional","affiliation":[]},{"given":"Jim","family":"Woodcock","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,10,22]]},"reference":[{"key":"28_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1007\/978-3-030-31038-7_5","volume-title":"Unifying Theories of Programming","author":"J Woodcock","year":"2019","unstructured":"Woodcock, J., Cavalcanti, A., Foster, S., Mota, A., Ye, K.: Probabilistic semantics for RoboChart. In: Ribeiro, P., Sampaio, A. (eds.) UTP 2019. LNCS, vol. 11885, pp. 80\u2013105. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31038-7_5"},{"issue":"5","key":"28_CR2","doi-asserted-by":"publisher","first-page":"3097","DOI":"10.1007\/s10270-018-00710-z","volume":"18","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019)","journal-title":"Softw. Syst. Model."},{"key":"28_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-540-30482-1_17","volume-title":"Formal Methods and Software Engineering","author":"H Jifeng","year":"2004","unstructured":"Jifeng, H., Morgan, C., McIver, A.: Deriving probabilistic semantics via the \u2018weakest completion\u2019. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 131\u2013145. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-30482-1_17"},{"key":"28_CR4","volume-title":"Unifying Theories of Programming","author":"CAR Hoare","year":"1998","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice-Hall, Hoboken (1998)"},{"issue":"2","key":"28_CR5","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1016\/0020-0190(87)90106-2","volume":"24","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127\u2013132 (1987)","journal-title":"Inf. Process. Lett."},{"key":"28_CR6","doi-asserted-by":"publisher","first-page":"102510","DOI":"10.1016\/j.scico.2020.102510","volume":"197","author":"S Foster","year":"2020","unstructured":"Foster, S., Baxter, J., Cavalcanti, A., Woodcock, J., Zeyda, F.: Unifying semantic foundations for automated verification tools in Isabelle\/UTP. Sci. Comput. Program. 197, 102510 (2020)","journal-title":"Sci. Comput. Program."},{"key":"28_CR7","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-order Logic. Springer, Cham (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"key":"28_CR8","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Introduction to pGCL: Its logic and Its Model. In: Abstraction, Refinement and Proof for Probabilistic Systems. Springer, New York, January 2005. https:\/\/doi.org\/10.1007\/0-387-27006-X_1","DOI":"10.1007\/0-387-27006-X_1"},{"key":"28_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"40","DOI":"10.1007\/978-3-540-24756-2_4","volume-title":"Integrated Formal Methods","author":"J Woodcock","year":"2004","unstructured":"Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40\u201366. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24756-2_4"},{"key":"28_CR10","doi-asserted-by":"publisher","unstructured":"Hehner, E.C.R.: A Practical Theory of Programming. Texts and Monographs in Computer Science. Springer, New York (1993). https:\/\/doi.org\/10.1007\/978-1-4419-8596-5","DOI":"10.1007\/978-1-4419-8596-5"},{"issue":"2","key":"28_CR11","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jlap.2009.07.002","volume":"79","author":"W Guttmann","year":"2010","unstructured":"Guttmann, W., M\u00f6ller, B.: Normal design algebra. J. Log. Algebraic Meth. Program. 79(2), 144\u2013173 (2010)","journal-title":"J. Log. Algebraic Meth. Program."},{"key":"28_CR12","unstructured":"H\u00f6lzl, J., Lochbihler, A.: Probability Mass Function. Technical Report https:\/\/isabelle.in.tum.de\/library\/HOL\/HOL-Probability\/Probability_Mass_Function.html"},{"key":"28_CR13","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Technical Report PRG44, OUCL, June 1985"},{"issue":"8","key":"28_CR14","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"EW Dijkstra","year":"1975","unstructured":"Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), 453\u2013457 (1975)","journal-title":"Commun. ACM"},{"issue":"2\u20133","key":"28_CR15","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/S0167-6423(96)00019-6","volume":"28","author":"H Jifeng","year":"1997","unstructured":"Jifeng, H., Seidel, K., McIver, A.: Probabilistic models for the guarded command language. Sci. Comput. Program. 28(2\u20133), 171\u2013192 (1997)","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"28_CR16","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Formal Meth. Syst. Des. 15(1), 7\u201348 (1999). https:\/\/doi.org\/10.1023\/A:1008739929481","journal-title":"Formal Meth. Syst. Des."},{"key":"28_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-540-27764-4_10","volume-title":"Mathematics of Program Construction","author":"ECR Hehner","year":"2004","unstructured":"Hehner, E.C.R.: Probabilistic predicative programming. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 169\u2013185. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27764-4_10"},{"key":"28_CR18","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Technical report, University of Cambridge, Computer Laboratory (2003)"},{"key":"28_CR19","volume-title":"Introduction to HOL: A Theorem Proving Environment for Higher Order Logic","year":"1993","unstructured":"Gordon, M.J.C., Melham, T.F. (eds.): Introduction to HOL: A Theorem Proving Environment for Higher Order Logic. Cambridge University Press, Cambridge (1993)"},{"issue":"1","key":"28_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., Morgan, C.: Probabilistic guarded commands mechanized in HOL. Theor. Comput. Sci. 346(1), 96\u2013112 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"28_CR21","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1145\/229542.229547","volume":"18","author":"C Morgan","year":"1996","unstructured":"Morgan, C., McIver, A., Seidel, K.: Probabilistic predicate transformers. ACM Trans. Program. Lang. Syst. (TOPLAS) 18(3), 325\u2013353 (1996)","journal-title":"ACM Trans. Program. Lang. Syst. (TOPLAS)"},{"issue":"8","key":"28_CR22","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009)","journal-title":"Sci. Comput. Program."},{"key":"28_CR23","unstructured":"The Coq development team: The Coq Proof Assistant. https:\/\/coq.inria.fr. Accessed 20 May 2021"},{"key":"28_CR24","doi-asserted-by":"crossref","unstructured":"Cock, D.: Verifying Probabilistic Correctness in Isabelle with pGCL. In Cassez, F., Huuck, R., Klein, G., Schlich, B., (eds.): Proceedings Seventh Conference on Systems Software Verification, SSV 2012, Sydney, Australia, 28\u201330 November 2012, volume 102 of EPTCS, pp. 167\u2013178 (2012)","DOI":"10.4204\/EPTCS.102.15"},{"key":"28_CR25","doi-asserted-by":"publisher","unstructured":"McIver, A., Morgan, C.: Abstraction, Refinement and Proof for Probabilistic Systems. Monographs in Computer Science. Springer, New York (2005). https:\/\/doi.org\/10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"28_CR26","series-title":"Emergence, Complexity and Computation","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-030-15792-0_10","volume-title":"From Astrophysics to Unconventional Computation","author":"K Ye","year":"2020","unstructured":"Ye, K., Foster, S., Woodcock, J.: Compositional assume-guarantee reasoning of control law diagrams using UTP. In: Adamatzky, A., Kendon, V. (eds.) From Astrophysics to Unconventional Computation. ECC, vol. 35, pp. 215\u2013254. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-15792-0_10"}],"container-title":["Lecture Notes in Computer Science","Relational and Algebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-88701-8_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,22]],"date-time":"2021-10-22T00:53:36Z","timestamp":1634864016000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-88701-8_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030887001","9783030887018"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-88701-8_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"22 October 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"RAMiCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Relational and Algebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Marseille","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2 November 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 November 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ramics2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ramics19.lis-lab.fr\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}