{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,26]],"date-time":"2025-03-26T18:48:18Z","timestamp":1743014898534,"version":"3.40.3"},"publisher-location":"Cham","reference-count":124,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031404351"},{"type":"electronic","value":"9783031404368"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-40436-8_2","type":"book-chapter","created":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:04:03Z","timestamp":1694127843000},"page":"19-51","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["UTP, Circus, and\u00a0Isabelle"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-7955-2702","authenticated-orcid":false,"given":"Jim","family":"Woodcock","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0831-1976","authenticated-orcid":false,"given":"Ana","family":"Cavalcanti","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9889-9514","authenticated-orcid":false,"given":"Simon","family":"Foster","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3023-2748","authenticated-orcid":false,"given":"Marcel","family":"Oliveira","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9870-6893","authenticated-orcid":false,"given":"Augusto","family":"Sampaio","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-4251-4740","authenticated-orcid":false,"given":"Frank","family":"Zeyda","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,9,8]]},"reference":[{"key":"2_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/BFb0027252","volume-title":"Formal Methods for Industrial Applications","author":"J-R Abrial","year":"1996","unstructured":"Abrial, J.-R.: Steam-boiler control specification problem. In: Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.) Formal Methods for Industrial Applications. LNCS, vol. 1165, pp. 500\u2013509. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0027252"},{"key":"2_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0027227","volume-title":"Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control","year":"1996","unstructured":"Abrial, J.-R., B\u00f6rger, E., Langmaack, H. (eds.): Formal Methods for Industrial Applications: Specifying and Programming the Steam Boiler Control. LNCS, vol. 1165. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0027227"},{"unstructured":"Althoff, M.: An introduction to CORA 2015. In: Frehse, G., Althoff, M. (eds.) 1st and 2nd International Workshop on Applied Verification for Continuous and Hybrid Systems. EPiC Series in Computing, vol. 34, pp. 120\u2013151. EasyChair (2015)","key":"2_CR3"},{"unstructured":"Arthan, R.: ProofPower. Lemma 1 Ltd. (2017). https:\/\/www.lemma-one.com\/ProofPower\/index\/","key":"2_CR4"},{"doi-asserted-by":"publisher","unstructured":"Atiya, D.M., King, S.: A compliance notation for verifying concurrent systems. In: Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, pp. 731\u2013732. Association for Computing Machinery (2002). https:\/\/doi.org\/10.1145\/581339.581475","key":"2_CR5","DOI":"10.1145\/581339.581475"},{"key":"2_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"617","DOI":"10.1007\/978-3-540-45236-2_34","volume-title":"FME 2003: Formal Methods","author":"D-A Atiya","year":"2003","unstructured":"Atiya, D.-A., King, S., Woodcock, J.C.P.: A Circus semantics for Ravenscar protected objects. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 617\u2013635. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45236-2_34"},{"key":"2_CR7","series-title":"Graduate Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2","volume-title":"Refinement Calculus: A Systematic Introduction","author":"RJR Back","year":"1998","unstructured":"Back, R.J.R., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science, Springer, New York (1998). https:\/\/doi.org\/10.1007\/978-1-4612-1674-2"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1007\/BF01558665","volume":"3","author":"R Back","year":"1989","unstructured":"Back, R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. Distrib. Comput. 3(2), 73\u201387 (1989). https:\/\/doi.org\/10.1007\/BF01558665","journal-title":"Distrib. Comput."},{"unstructured":"Baltag, A., Moss, L.S., Solecki, S.: The logic of public announcements and common knowledge and private suspicions. In: Gilboa, I. (ed.) Proceedings of the 7th Conference on Theoretical Aspects of Rationality and Knowledge (TARK-1998), Evanston, IL, USA, 22\u201324 July 1998, pp. 43\u201356. Morgan Kaufmann (1998)","key":"2_CR9"},{"unstructured":"Barnes, J.: Programming in ADA 95, 2nd edn. Addison-Wesley (1998)","key":"2_CR10"},{"unstructured":"Barrocas, S.L.M., Oliveira, M.V.M.: JCircus 2.0: an extension of an automatic translator from Circus to Java. In: Welch, P.H., Barnes, F.R.M., Chalmers, K., Pedersen, J.B., Sampson, A.T. (eds.) 34th Communicating Process Architectures, CPA 2012, Organised Under the Auspices of WoTUG, Dundee, Scotland, UK, 26 August 2012, pp. 15\u201336. Open Channel Publishing Ltd. (2012)","key":"2_CR11"},{"unstructured":"Bauer, J.C.: Specification for a software program for a boiler water content monitor and control system. Technical report, Institute of Risk Research, University of Waterloo (1993)","key":"2_CR12"},{"unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: 3rd International Conference on the Quantitative Evaluation of Systems, pp. 125\u2013126. IEEE Computer Society (2006)","key":"2_CR13"},{"key":"2_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/BFb0055011","volume-title":"Reliable Software Technologies \u2014 Ada-Europe","author":"A Burns","year":"1998","unstructured":"Burns, A., Dobbing, B., Romanski, G.: The Ravenscar tasking profile for high integrity real-time programs. In: Asplund, L. (ed.) Ada-Europe 1998. LNCS, vol. 1411, pp. 263\u2013275. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0055011"},{"doi-asserted-by":"crossref","unstructured":"Butterfield, A., Gancarski, P., Woodcock, J.C.P.: State visibility and communication in unifying theories of programming. In: Chin, W.N., Qin, S. (eds.) 3rd IEEE International Symposium on Theoretical Aspects of Software Engineering, pp. 47\u201354. IEEE Computer Society (2009)","key":"2_CR15","DOI":"10.1109\/TASE.2009.57"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-540-73210-5_5","volume-title":"Integrated Formal Methods","author":"A Butterfield","year":"2007","unstructured":"Butterfield, A., Sherif, A., Woodcock, J.: Slotted-Circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75\u201397. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73210-5_5"},{"doi-asserted-by":"publisher","unstructured":"Butterfield, A., Woodcock, J.: Semantic domains for Handel-C. In: Flynn, S., et al. (eds.) Second Irish Conference on the Mathematical Foundations of Computer Science and Information Technology, MFCSIT 2002. Electronic Notes in Theoretical Computer Science, Galway, Ireland, 18\u201319 July 2002, vol. 74, pp. 1\u201320. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(04)80762-X","key":"2_CR17","DOI":"10.1016\/S1571-0661(04)80762-X"},{"issue":"3","key":"2_CR18","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/s10009-004-0181-6","volume":"7","author":"A Butterfield","year":"2005","unstructured":"Butterfield, A., Woodcock, J.: prialt in Handel-C: an operational semantics. Int. J. Softw. Tools Technol. Transf. 7(3), 248\u2013267 (2005). https:\/\/doi.org\/10.1007\/s10009-004-0181-6","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"2_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-14806-9_1","volume-title":"Unifying Theories of Programming","author":"S Canham","year":"2015","unstructured":"Canham, S., Woodcock, J.: Three approaches to timed external choice in UTP. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 1\u201320. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-14806-9_1"},{"key":"2_CR20","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/978-3-030-66494-7_9","volume-title":"Software Engineering for Robotics","author":"A Cavalcanti","year":"2021","unstructured":"Cavalcanti, A., et al.: RoboStar technology: a roboticist\u2019s toolbox for combined proof, simulation, and testing. In: Cavalcanti, A., Dongol, B., Hierons, R., Timmis, J., Woodcock, J. (eds.) Software Engineering for Robotics, pp. 249\u2013293. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-66494-7_9"},{"key":"2_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/978-3-030-92124-8_1","volume-title":"Software Engineering and Formal Methods","author":"A Cavalcanti","year":"2021","unstructured":"Cavalcanti, A., Baxter, J., Carvalho, G.: RoboWorld: where can my robot work? In: Calinescu, R., P\u0103s\u0103reanu, C.S. (eds.) SEFM 2021. LNCS, vol. 13085, pp. 3\u201322. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-92124-8_1"},{"issue":"2","key":"2_CR22","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/s00236-011-0133-z","volume":"48","author":"ALC Cavalcanti","year":"2011","unstructured":"Cavalcanti, A.L.C., Gaudel, M.C.: Testing for refinement in Circus. Acta Informatica 48(2), 97\u2013147 (2011). https:\/\/doi.org\/10.1007\/s00236-011-0133-z","journal-title":"Acta Informatica"},{"issue":"2\u20133","key":"2_CR23","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"ALC Cavalcanti","year":"2003","unstructured":"Cavalcanti, A.L.C., Sampaio, A.C.A., Woodcock, J.C.P.: A refinement strategy for Circus. Formal Aspects Comput. 15(2\u20133), 146\u2013181 (2003). https:\/\/doi.org\/10.1007\/s00165-003-0006-5","journal-title":"Formal Aspects Comput."},{"key":"2_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/11889229_6","volume-title":"Refinement Techniques in Software Engineering","author":"A Cavalcanti","year":"2006","unstructured":"Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220\u2013268. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11889229_6"},{"issue":"3","key":"2_CR25","doi-asserted-by":"publisher","first-page":"288","DOI":"10.1007\/s00165-006-0001-8","volume":"18","author":"ALC Cavalcanti","year":"2006","unstructured":"Cavalcanti, A.L.C., Woodcock, J.C.P., Dunne, S.: Angelic nondeterminism in the unifying theories of programming. Formal Aspects Comput. 18(3), 288\u2013307 (2006). https:\/\/doi.org\/10.1007\/s00165-006-0001-8","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"publisher","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: Refinement of actions in Circus. In: Derrick, J., Boiten, E.A., Woodcock, J., von Wright, J. (eds.) BCS FACS Refinement Workshop 2002, Refine 2002, Satellite Event of FLoC 2002. Electronic Notes in Theoretical Computer Science, Copenhagen, Denmark, 20\u201321 July 2002, vol. 70, pp. 132\u2013162. Elsevier (2002). https:\/\/doi.org\/10.1016\/S1571-0661(05)80489-X","key":"2_CR26","DOI":"10.1016\/S1571-0661(05)80489-X"},{"issue":"2\u20133","key":"2_CR27","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/s00165-003-0006-5","volume":"15","author":"A Cavalcanti","year":"2003","unstructured":"Cavalcanti, A., Sampaio, A., Woodcock, J.: A refinement strategy for Circus. Formal Aspects Comput. 15(2\u20133), 146\u2013181 (2003). https:\/\/doi.org\/10.1007\/s00165-003-0006-5","journal-title":"Formal Aspects Comput."},{"issue":"3","key":"2_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/s001650050016","volume":"10","author":"A Cavalcanti","year":"1998","unstructured":"Cavalcanti, A., Woodcock, J.: ZRC \u2013 a refinement calculus for Z. Formal Aspects Comput. 10(3), 267\u2013289 (1998). https:\/\/doi.org\/10.1007\/s001650050016","journal-title":"Formal Aspects Comput."},{"issue":"2","key":"2_CR29","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1049\/ip-sen:20030131","volume":"150","author":"A Cavalcanti","year":"2003","unstructured":"Cavalcanti, A., Woodcock, J.: Predicate transformers in the semantics of Circus. IEE Proc. Softw. 150(2), 85\u201394 (2003). https:\/\/doi.org\/10.1049\/ip-sen:20030131","journal-title":"IEE Proc. Softw."},{"unstructured":"Copilot: Your AI pair programmer. GitHub. https:\/\/copilot.github.com. Accessed 18 June 2023","key":"2_CR30"},{"unstructured":"Dijkstra, E.W.: A Discipline of Programming. Prentice Hall (1976). https:\/\/www.worldcat.org\/oclc\/01958445l","key":"2_CR31"},{"key":"2_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-16690-7_9","volume-title":"Unifying Theories of Programming","author":"A Feliachi","year":"2010","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Unifying theories in Isabelle\/HOL. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 188\u2013206. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16690-7_9"},{"unstructured":"Feliachi, A., Gaudel, M.C., Wolff, B.: Exhaustive testing in HOL-Testgen\/CirTa \u2013 a case study. Technical report 1562, LRI, July 2013","key":"2_CR33"},{"unstructured":"Feliachi, A.: Semantics-based testing for Circus. (Test bas\u00e9 sur la s\u00e9mantique pour Circus). Ph.D. thesis, University of Paris-Sud, Orsay, France (2012). https:\/\/theses.hal.science\/tel-00821836","key":"2_CR34"},{"key":"2_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-642-41202-8_10","volume-title":"Formal Methods and Software Engineering","author":"A Feliachi","year":"2013","unstructured":"Feliachi, A., Gaudel, M.-C., Wenzel, M., Wolff, B.: The Circus testing theory revisited in Isabelle\/HOL. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 131\u2013147. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-41202-8_10"},{"key":"2_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-27705-4_20","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Feliachi","year":"2012","unstructured":"Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle\/Circus: a process specification and verification environment. In: Joshi, R., M\u00fcller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243\u2013260. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-27705-4_20"},{"unstructured":"Feliachi, A., Wolff, B., Gaudel, M.: Isabelle\/Circus. Arch. Formal Proofs 2012 (2012). https:\/\/www.isa-afp.org\/entries\/Circus.shtml","key":"2_CR37"},{"key":"2_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/978-3-540-49676-2_2","volume-title":"ZUM \u201998: The Z Formal Specification Notation","author":"C Fischer","year":"1998","unstructured":"Fischer, C.: How to combine Z with a process algebra. In: Bowen, J.P., Fett, A., Hinchey, M.G. (eds.) ZUM 1998. LNCS, vol. 1493, pp. 5\u201323. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/978-3-540-49676-2_2"},{"key":"2_CR39","first-page":"92","volume":"71","author":"C Fischer","year":"2000","unstructured":"Fischer, C., Wehrheim, H.: Failure-divergence semantics as a formal basis for an object-oriented integrated formal method. Bull. EATCS 71, 92\u2013101 (2000)","journal-title":"Bull. EATCS"},{"unstructured":"Foster, J.: Bidirectional programming languages. Ph.D. thesis, University of Pennsylvania (2009)","key":"2_CR40"},{"key":"2_CR41","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"130","DOI":"10.1007\/978-3-030-31038-7_7","volume-title":"Unifying Theories of Programming","author":"S Foster","year":"2019","unstructured":"Foster, S.: Hybrid relations in Isabelle\/UTP. In: Ribeiro, P., Sampaio, A. (eds.) UTP 2019. LNCS, vol. 11885, pp. 130\u2013153. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31038-7_7"},{"key":"2_CR42","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/j.tcs.2019.09.017","volume":"802","author":"S Foster","year":"2020","unstructured":"Foster, S., Cavalcanti, A.L.C., Canham, S., Woodcock, J.C.P., Zeyda, F.: Unifying theories of reactive design contracts. Theor. Comput. Sci. 802, 105\u2013140 (2020). https:\/\/doi.org\/10.1016\/j.tcs.2019.09.017","journal-title":"Theor. Comput. Sci."},{"key":"2_CR43","doi-asserted-by":"publisher","first-page":"47","DOI":"10.1016\/j.ipl.2018.02.017","volume":"135","author":"S Foster","year":"2018","unstructured":"Foster, S., Cavalcanti, A.L.C., Woodcock, J.C.P., Zeyda, F.: Unifying theories of time with generalised reactive processes. Inf. Process. Lett. 135, 47\u201352 (2018). https:\/\/doi.org\/10.1016\/j.ipl.2018.02.017","journal-title":"Inf. Process. Lett."},{"key":"2_CR44","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100681","volume":"121","author":"S Foster","year":"2021","unstructured":"Foster, S., Ye, K., Cavalcanti, A.L.C., Woodcock, J.C.P.: Automated verification of reactive and concurrent programs by calculation. J. Log. Algebraic Methods Program. 121, 100681 (2021). https:\/\/doi.org\/10.1016\/j.jlamp.2021.100681","journal-title":"J. Log. Algebraic Methods Program."},{"key":"2_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1007\/978-3-319-14806-9_2","volume-title":"Unifying Theories of Programming","author":"S Foster","year":"2015","unstructured":"Foster, S., Zeyda, F., Woodcock, J.: Isabelle\/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21\u201341. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-14806-9_2"},{"key":"2_CR46","doi-asserted-by":"publisher","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). https:\/\/doi.org\/10.1016\/j.scico.2020.102510","journal-title":"Sci. Comput. Program."},{"doi-asserted-by":"publisher","unstructured":"Foster, S., Hur, C., Woodcock, J.: Formally verified simulations of state-rich processes using interaction trees in Isabelle\/HOL. In: Haddad, S., Varacca, D. (eds.) 32nd International Conference on Concurrency Theory, CONCUR 2021. LIPIcs, 24\u201327 August 2021, Virtual Conference, vol. 203, pp. 20:1\u201320:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.20","key":"2_CR47","DOI":"10.4230\/LIPIcs.CONCUR.2021.20"},{"key":"2_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-90870-6_20","volume-title":"Formal Methods","author":"S Foster","year":"2021","unstructured":"Foster, S., Huerta y Munive, J.J., Gleirscher, M., Struth, G.: Hybrid systems verification with Isabelle\/HOL: simpler syntax, better models, faster proofs. In: Huisman, M., P\u0103s\u0103reanu, C., Zhan, N. (eds.) FM 2021. LNCS, vol. 13047, pp. 367\u2013386. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-90870-6_20"},{"key":"2_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/978-3-319-46750-4_17","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2016","author":"S Foster","year":"2016","unstructured":"Foster, S., Zeyda, F., Woodcock, J.: Unifying heterogeneous state-spaces with lenses. In: Sampaio, A., Wang, F. (eds.) ICTAC 2016. LNCS, vol. 9965, pp. 295\u2013314. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46750-4_17"},{"key":"2_CR50","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/11813040_9","volume-title":"FM 2006: Formal Methods","author":"A Freitas","year":"2006","unstructured":"Freitas, A., Cavalcanti, A.: Automatic translation from Circus to Java. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006. LNCS, vol. 4085, pp. 115\u2013130. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11813040_9"},{"unstructured":"Freitas, L.J.S.: Model checking Circus. Ph.D. thesis, University of York, Department of Computer Science (2006)","key":"2_CR51"},{"issue":"5","key":"2_CR52","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1007\/s10009-011-0195-9","volume":"13","author":"L Freitas","year":"2011","unstructured":"Freitas, L., McDermott, J.P.: Formal methods for security in the Xenon hypervisor. Int. J. Softw. Tools Technol. Transf. 13(5), 463\u2013489 (2011). https:\/\/doi.org\/10.1007\/s10009-011-0195-9","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"2","key":"2_CR53","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/s10009-015-0377-y","volume":"18","author":"T Gibson-Robinson","year":"2016","unstructured":"Gibson-Robinson, T., Armstrong, P.J., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol. Transf. 18(2), 149\u2013167 (2016). https:\/\/doi.org\/10.1007\/s10009-015-0377-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"doi-asserted-by":"publisher","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: Proceedings of the 1984 IEEE Symposium on Security and Privacy, Oakland, California, USA, 29 April\u20132 May 1984, pp. 75\u201387. IEEE Computer Society (1984). https:\/\/doi.org\/10.1109\/SP.1984.10019","key":"2_CR54","DOI":"10.1109\/SP.1984.10019"},{"issue":"2","key":"2_CR55","doi-asserted-by":"publisher","first-page":"144","DOI":"10.1016\/j.jlap.2009.07.002","volume":"79","author":"W Guttman","year":"2010","unstructured":"Guttman, W., M\u00f6ller, B.: Normal design algebra. J. Log. Algebraic Program. 79(2), 144\u2013173 (2010)","journal-title":"J. Log. Algebraic Program."},{"key":"2_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-85762-4_10","volume-title":"Theoretical Aspects of Computing - ICTAC 2008","author":"W Harwood","year":"2008","unstructured":"Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141\u2013155. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-85762-4_10"},{"unstructured":"Henkin, L., Monk, J., Tarski, A.: Cylindric Algebras, Part I. North-Holland (1971)","key":"2_CR57"},{"unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall (1985)","key":"2_CR58"},{"unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall (1998)","key":"2_CR59"},{"unstructured":"Jones, G., Goldsmith, M.: Programming in OCCAM 2. International Series in Computer Science. Prentice Hall (1985)","key":"2_CR60"},{"issue":"1\u20132","key":"2_CR61","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1016\/S0004-3702(98)00023-X","volume":"101","author":"LP Kaelbling","year":"1998","unstructured":"Kaelbling, L.P., Littman, M.L., Cassandra, A.R.: Planning and acting in partially observable stochastic domains. Artif. Intell. 101(1\u20132), 99\u2013134 (1998). https:\/\/doi.org\/10.1016\/S0004-3702(98)00023-X","journal-title":"Artif. Intell."},{"unstructured":"King, S., S\u00f8rensen, l.H., Woodcock, J.: Z, Grammar and Concrete and Abstract Syntaxes. Technical Monograph PRG-68. Oxford University Computing Laboratory, Programming Research Group (1988)","key":"2_CR62"},{"key":"2_CR63","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39718-9","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2013","year":"2013","unstructured":"Liu, Z., Woodcock, J., Zhu, H. (eds.): ICTAC 2013. LNCS, vol. 8049. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39718-9"},{"key":"2_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39698-4","volume-title":"Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday","year":"2013","unstructured":"Liu, Z., Woodcock, J., Zhu, H. (eds.): Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 70th Birthday. LNCS, vol. 8051. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4"},{"key":"2_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39721-9","volume-title":"Unifying Theories of Programming and Formal Engineering Methods","year":"2013","unstructured":"Liu, Z., Woodcock, J., Zhu, H. (eds.): Unifying Theories of Programming and Formal Engineering Methods. LNCS, vol. 8050. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39721-9"},{"unstructured":"Locke, D., et al.: Safety-Critical Java Technology Specification, Public Draft. Java Community Process (2011)","key":"2_CR66"},{"unstructured":"Celoxica Ltd.: DK3: Handel-C Language Reference Manual (2002)","key":"2_CR67"},{"key":"2_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/3-540-48753-0_2","volume-title":"Reliable Software Technologies \u2014 Ada-Europe\u2019 99","author":"K Lundqvist","year":"1999","unstructured":"Lundqvist, K., Asplund, L., Michell, S.: A formal model of the Ada Ravenscar tasking profile; protected objects. In: Gonz\u00e1lez Harbour, M., de la Puente, J.A. (eds.) Ada-Europe 1999. LNCS, vol. 1622, pp. 12\u201325. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48753-0_2"},{"doi-asserted-by":"publisher","unstructured":"McDermott, J.P., Freitas, L.: Using formal methods for security in the Xenon project. In: Sheldon, F.T., Prowell, S.J., Abercrombie, R.K., Krings, A.W. (eds.) Proceedings of the 6th Cyber Security and Information Intelligence Research Workshop, CSIIRW 2010, Oak Ridge, TN, USA, 21\u201323 April 2010, p. 67. ACM (2010). https:\/\/doi.org\/10.1145\/1852666.1852742","key":"2_CR69","DOI":"10.1145\/1852666.1852742"},{"issue":"1","key":"2_CR70","doi-asserted-by":"publisher","first-page":"17","DOI":"10.1016\/j.istr.2008.01.001","volume":"13","author":"JP McDermott","year":"2008","unstructured":"McDermott, J.P., Kirby, J., Montrose, B.E., Johnson, T., Kang, M.H.: Re-engineering Xen internals for higher-assurance security. Inf. Secur. Tech. Rep. 13(1), 17\u201324 (2008). https:\/\/doi.org\/10.1016\/j.istr.2008.01.001","journal-title":"Inf. Secur. Tech. Rep."},{"issue":"5","key":"2_CR71","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.L.C., Timmis, J., Woodcock, J.C.P.: RoboChart: modelling and verification of the functional behaviour of robotic applications. Softw. Syst. Model. 18(5), 3097\u20133149 (2019). https:\/\/doi.org\/10.1007\/s10270-018-00710-z","journal-title":"Softw. Syst. Model."},{"key":"2_CR72","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/j.scico.2019.01.002","volume":"181","author":"A Miyazawa","year":"2019","unstructured":"Miyazawa, A., Cavalcanti, A., Wellings, A.J.: SCJ-Circus: specification and refinement of safety-critical Java programs. Sci. Comput. Program. 181, 140\u2013176 (2019). https:\/\/doi.org\/10.1016\/j.scico.2019.01.002","journal-title":"Sci. Comput. Program."},{"issue":"5","key":"2_CR73","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1016\/0020-0190(88)90147-0","volume":"26","author":"C Morgan","year":"1988","unstructured":"Morgan, C.: Data refinement by miracles. Inf. Process. Lett. 26(5), 243\u2013246 (1988). https:\/\/doi.org\/10.1016\/0020-0190(88)90147-0","journal-title":"Inf. Process. Lett."},{"key":"2_CR74","series-title":"Texts and Monographs in Computer Science","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/978-1-4612-4476-9_37","volume-title":"Beauty Is Our Business","author":"C Morgan","year":"1990","unstructured":"Morgan, C.: Of wp and CSP. In: Feijen, W.H.J., van Gasteren, A.J.M., Gries, D., Misra, J. (eds.) Beauty Is Our Business. MCS, pp. 319\u2013326. Springer, New York (1990). https:\/\/doi.org\/10.1007\/978-1-4612-4476-9_37"},{"unstructured":"Morgan, C.: Programming from Specifications. International Series in Computer Science, 2nd edn. Prentice Hall (1994)","key":"2_CR75"},{"issue":"3","key":"2_CR76","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1016\/0167-6423(87)90011-6","volume":"9","author":"JM Morris","year":"1987","unstructured":"Morris, J.M.: A theoretical basis for stepwise refinement and the programming calculus. Sci. Comput. Program. 9(3), 287\u2013306 (1987). https:\/\/doi.org\/10.1016\/0167-6423(87)90011-6","journal-title":"Sci. Comput. Program."},{"key":"2_CR77","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"169","DOI":"10.1007\/978-3-030-43520-2_11","volume-title":"Relational and Algebraic Methods in Computer Science","author":"S Foster","year":"2020","unstructured":"Foster, S., Huerta y Munive, J.J., Struth, G.: Differential Hoare logics and refinement calculi for hybrid systems with Isabelle\/HOL. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds.) RAMiCS 2020. LNCS, vol. 12062, pp. 169\u2013186. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_11"},{"unstructured":"O\u2019Halloran, C.: Identifying critical requirements. Technical report, Systems Assurance Group, QinetiQ Malvern (2002)","key":"2_CR78"},{"unstructured":"Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York, UK (2005). https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.428459","key":"2_CR79"},{"unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Refining industrial scale systems in Circus. In: East, I., Martin, J., Welch, P., Duce, D., Green, M. (eds.) Communicating Process Architectures. Concurrent Systems Engineering Series, vol. 62, pp. 281\u2013309. IOS Press (2004)","key":"2_CR80"},{"issue":"2","key":"2_CR81","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1007\/s11334-005-0014-0","volume":"1","author":"MVM Oliveira","year":"2005","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Formal development of industrial-scale systems in Circus. Innov. Syst. Softw. Eng. 1(2), 125\u2013146 (2005). https:\/\/doi.org\/10.1007\/s11334-005-0014-0","journal-title":"Innov. Syst. Softw. Eng."},{"doi-asserted-by":"publisher","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A denotational semantics for Circus. In: Aichernig, B.K., Boiten, E.A., Derrick, J., Groves, L. (eds.) Proceedings of the 11th Refinement Workshop, Refine@ICFEM 2006. Electronic Notes in Theoretical Computer Science, Macao, 31 October 2006, vol. 187, pp. 107\u2013123. Elsevier (2006). https:\/\/doi.org\/10.1016\/j.entcs.2006.08.047","key":"2_CR82","DOI":"10.1016\/j.entcs.2006.08.047"},{"issue":"1\u20132","key":"2_CR83","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00165-007-0052-5","volume":"21","author":"MVM Oliveira","year":"2009","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP semantics for Circus. Formal Aspects Comput. 21(1\u20132), 3\u201332 (2009). https:\/\/doi.org\/10.1007\/s00165-007-0052-5","journal-title":"Formal Aspects Comput."},{"issue":"1","key":"2_CR84","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1007\/s00165-007-0044-5","volume":"25","author":"MVM Oliveira","year":"2013","unstructured":"Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: Unifying theories in ProofPower-Z. Formal Aspects Comput. 25(1), 133\u2013158 (2013). https:\/\/doi.org\/10.1007\/s00165-007-0044-5","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"publisher","unstructured":"Ribeiro, P., Cavalcanti, A.L.C.: Designs with angelic nondeterminism. In: 7th International Symposium on Theoretical Aspects of Software Engineering, pp. 71\u201378. IEEE (2013). https:\/\/doi.org\/10.1109\/TASE.2013.18","key":"2_CR85","DOI":"10.1109\/TASE.2013.18"},{"key":"2_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"42","DOI":"10.1007\/978-3-319-14806-9_3","volume-title":"Unifying Theories of Programming","author":"P Ribeiro","year":"2015","unstructured":"Ribeiro, P., Cavalcanti, A.: Angelicism in the theory of reactive processes. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 42\u201361. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-14806-9_3"},{"key":"2_CR87","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/j.tcs.2018.10.008","volume":"756","author":"P Ribeiro","year":"2019","unstructured":"Ribeiro, P., Cavalcanti, A.L.C.: Angelic processes for CSP via the UTP. Theor. Comput. Sci. 756, 19\u201363 (2019). https:\/\/doi.org\/10.1016\/j.tcs.2018.10.008","journal-title":"Theor. Comput. Sci."},{"key":"2_CR88","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"270","DOI":"10.1007\/978-3-030-43520-2_17","volume-title":"Relational and Algebraic Methods in Computer Science","author":"P Ribeiro","year":"2020","unstructured":"Ribeiro, P.: A unary semigroup trace algebra. In: Fahrenberg, U., Jipsen, P., Winter, M. (eds.) RAMiCS 2020. LNCS, vol. 12062, pp. 270\u2013285. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-43520-2_17"},{"key":"2_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/3-540-15670-4_15","volume-title":"Seminar on Concurrency","author":"AW Roscoe","year":"1985","unstructured":"Roscoe, A.W.: Denotational semantics for occam. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) CONCURRENCY 1984. LNCS, vol. 197, pp. 306\u2013329. Springer, Heidelberg (1985). https:\/\/doi.org\/10.1007\/3-540-15670-4_15"},{"unstructured":"Roscoe, A.W.: The Theory and Practice of Concurrency. Series in Computer Science. Prentice Hall (1997)","key":"2_CR90"},{"key":"2_CR91","series-title":"Texts in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-84882-258-0","volume-title":"Understanding Concurrent Systems","author":"AW Roscoe","year":"2010","unstructured":"Roscoe, A.W.: Understanding Concurrent Systems. Texts in Computer Science, Springer, London (2010). https:\/\/doi.org\/10.1007\/978-1-84882-258-0"},{"key":"2_CR92","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/0304-3975(88)90049-7","volume":"60","author":"AW Roscoe","year":"1988","unstructured":"Roscoe, A.W., Hoare, C.A.R.: The laws of OCCAM programming. Theor. Comput. Sci. 60, 177\u2013229 (1988). https:\/\/doi.org\/10.1016\/0304-3975(88)90049-7","journal-title":"Theor. Comput. Sci."},{"key":"2_CR93","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/3-540-58618-0_55","volume-title":"Computer Security \u2014 ESORICS 94","author":"AW Roscoe","year":"1994","unstructured":"Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 31\u201353. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58618-0_55"},{"key":"2_CR94","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"451","DOI":"10.1007\/3-540-45614-7_26","volume-title":"FME 2002:Formal Methods\u2014Getting IT Right","author":"A Sampaio","year":"2002","unstructured":"Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 451\u2013470. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45614-7_26"},{"issue":"4","key":"2_CR95","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/s00165-005-0076-7","volume":"17","author":"SA Schneider","year":"2005","unstructured":"Schneider, S.A., Treharne, H.: CSP theorems for communicating B machines. Formal Aspects Comput. 17(4), 390\u2013422 (2005). https:\/\/doi.org\/10.1007\/s00165-005-0076-7","journal-title":"Formal Aspects Comput."},{"key":"2_CR96","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"613","DOI":"10.1007\/3-540-36103-0_62","volume-title":"Formal Methods and Software Engineering","author":"A Sherif","year":"2002","unstructured":"Sherif, A., Jifeng, H.: Towards a time model for Circus. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613\u2013624. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36103-0_62"},{"key":"2_CR97","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-540-31862-0_34","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"A Sherif","year":"2005","unstructured":"Sherif, A., Jifeng, H., Cavalcanti, A., Sampaio, A.: A framework for specification and validation of real-time systems using Circus actions. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 478\u2013493. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_34"},{"unstructured":"Shilov, N.V., Garanina, N.O.: Combining knowledge and fixpoints. Technical report preprint 98, A.P. Ershov Institute of Informatics Systems, Novosibirsk (2002). https:\/\/www.iis.nsk.su\/files\/preprints\/098.pdf","key":"2_CR98"},{"key":"2_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-63533-5_4","volume-title":"FME \u201997: Industrial Applications and Strengthened Foundations of Formal Methods","author":"G Smith","year":"1997","unstructured":"Smith, G.: A semantic integration of object-Z and CSP for the specification of concurrent systems. In: Fitzgerald, J., Jones, C.B., Lucas, P. (eds.) FME 1997. LNCS, vol. 1313, pp. 62\u201381. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63533-5_4"},{"unstructured":"Spivey, J.M.: Z Notation \u2013 A Reference Manual. International Series in Computer Science, 2nd edn. Prentice Hall (1992)","key":"2_CR100"},{"key":"2_CR101","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/11783596_25","volume-title":"Mathematics of Program Construction","author":"A Tafliovich","year":"2006","unstructured":"Tafliovich, A., Hehner, E.C.R.: Quantum predicative programming. In: Uustalu, T. (ed.) MPC 2006. LNCS, vol. 4014, pp. 433\u2013454. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11783596_25"},{"key":"2_CR102","volume-title":"Probabilistic Robotics. Intelligent Robotics and Autonomous Agents","author":"S Thrun","year":"2005","unstructured":"Thrun, S., Burgard, W., Fox, D.: Probabilistic Robotics. Intelligent Robotics and Autonomous Agents. MIT Press, Cambridge (2005)"},{"doi-asserted-by":"publisher","unstructured":"Wei, K., Woodcock, J., Burns, A.: A timed model of Circus with the reactive design miracle. In: Fiadeiro, J.L., Gnesi, S., Maggiolo-Schettini, A. (eds.) 8th IEEE International Conference on Software Engineering and Formal Methods, SEFM 2010, Pisa, Italy, 13\u201318 September 2010, pp. 315\u2013319. IEEE Computer Society (2010). https:\/\/doi.org\/10.1109\/SEFM.2010.40","key":"2_CR103","DOI":"10.1109\/SEFM.2010.40"},{"doi-asserted-by":"publisher","unstructured":"Wei, K., Woodcock, J., Burns, A.: Timed Circus: timed CSP with the miracle. In: Perseil, I., Breitman, K.K., Sterritt, R. (eds.) 16th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2011, Las Vegas, Nevada, USA, 27\u201329 April 2011, pp. 55\u201364. IEEE Computer Society (2011). https:\/\/doi.org\/10.1109\/ICECCS.2011.13","key":"2_CR104","DOI":"10.1109\/ICECCS.2011.13"},{"key":"2_CR105","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"687","DOI":"10.1007\/3-540-46080-2_72","volume-title":"Computational Science \u2014 ICCS 2002","author":"P Welch","year":"2002","unstructured":"Welch, P.: Process oriented design for Java: concurrency for all. In: Sloot, P.M.A., Hoekstra, A.G., Tan, C.J.K., Dongarra, J.J. (eds.) ICCS 2002. LNCS, vol. 2330, pp. 687\u2013687. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46080-2_72"},{"key":"2_CR106","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"695","DOI":"10.1007\/3-540-46080-2_74","volume-title":"Computational Science \u2014 ICCS 2002","author":"PH Welch","year":"2002","unstructured":"Welch, P.H., Aldous, J.R., Foster, J.: CSP networking for Java (JCSP.net). In: Sloot, P.M.A., Hoekstra, A.G., Tan, C.J.K., Dongarra, J.J. (eds.) ICCS 2002. LNCS, vol. 2330, pp. 695\u2013708. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-46080-2_74"},{"issue":"5","key":"2_CR107","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1145\/71633.71634","volume":"14","author":"JCP Woodcock","year":"1989","unstructured":"Woodcock, J.C.P.: Properties of Z specifications. ACM SIGSOFT Softw. Eng. Notes 14(5), 43\u201354 (1989). https:\/\/doi.org\/10.1145\/71633.71634","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"unstructured":"Woodcock, J.C.P., Cavalcanti, A.L.C.: Circus: a concurrent refinement language. Technical report, Oxford University Computing Laboratory (2001)","key":"2_CR108"},{"key":"2_CR109","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"},{"unstructured":"Woodcock, J.C.P., Davies, J.: Using Z - Specification, Refinement, and Proof. International Series in Computer Science. Prentice Hall (1996)","key":"2_CR110"},{"doi-asserted-by":"publisher","unstructured":"Woodcock, J.: Using Circus for safety-critical applications. In: Cavalcanti, A., Machado, P.D.L. (eds.) Proceedings of the 6th Brazilian Workshop on Formal Methods, WMF 2003. Electronic Notes in Theoretical Computer Science, Campina Grande, Brazil, 12\u201314 October 2003, vol. 95, pp. 3\u201322. Elsevier (2003). https:\/\/doi.org\/10.1016\/j.entcs.2004.04.003","key":"2_CR111","DOI":"10.1016\/j.entcs.2004.04.003"},{"key":"2_CR112","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-14521-6_12","volume-title":"Unifying Theories of Programming","author":"J Woodcock","year":"2010","unstructured":"Woodcock, J.: The miracle of reactive programming. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 202\u2013217. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14521-6_12"},{"doi-asserted-by":"publisher","unstructured":"Woodcock, J.: Hoare and He\u2019s unifying theories of programming. In: Jones, C.B., Misra, J. (eds.) Theories of Programming: The Life and Works of Tony Hoare, pp. 285\u2013316. ACM\/Morgan & Claypool (2021). https:\/\/doi.org\/10.1145\/3477355.3477369","key":"2_CR113","DOI":"10.1145\/3477355.3477369"},{"doi-asserted-by":"publisher","unstructured":"Woodcock, J., Cavalcanti, A.: A concurrent language for refinement. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, 16\u201317 July 2001. Workshops in Computing, BCS (2001). https:\/\/doi.org\/10.14236\/ewic\/IWFM2001.7","key":"2_CR114","DOI":"10.14236\/ewic\/IWFM2001.7"},{"doi-asserted-by":"publisher","unstructured":"Woodcock, J., Cavalcanti, A.: The steam boiler in a unified theory of Z and CSP. In: 8th Asia-Pacific Software Engineering Conference (APSEC 2001), Macau, China, 4\u20137 December 2001, pp. 291\u2013298. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/APSEC.2001.991490","key":"2_CR115","DOI":"10.1109\/APSEC.2001.991490"},{"key":"2_CR116","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/3-540-45648-1_10","volume-title":"ZB 2002:Formal Specification and Development in Z and B","author":"J Woodcock","year":"2002","unstructured":"Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184\u2013203. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45648-1_10"},{"key":"2_CR117","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":"2_CR118","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/11526841_17","volume-title":"FM 2005: Formal Methods","author":"J Woodcock","year":"2005","unstructured":"Woodcock, J., Cavalcanti, A., Freitas, L.: Operational semantics for model checking Circus. In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 237\u2013252. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11526841_17"},{"unstructured":"Woodcock, J., Davies, J., Bolton, C.: Abstract data types and processes. In: Roscoe, A.W., Davies, J., Woodcock, J. (eds.) Proceedings of the 1999 Oxford-Microsoft Symposium in Honour of Sir Tony Hoare. Millennial Perspectives in Computer Science, pp. 391\u2013405. Palgrave (2000)","key":"2_CR119"},{"key":"2_CR120","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"340","DOI":"10.1007\/3-540-52513-0_18","volume-title":"VDM \u201990 VDM and Z \u2014 Formal Methods in Software Development","author":"JCP Woodcock","year":"1990","unstructured":"Woodcock, J.C.P., Morgan, C.: Refinement of state-based concurrent systems. In: Bj\u00f8rner, D., Hoare, C.A.R., Langmaack, H. (eds.) VDM 1990. LNCS, vol. 428, pp. 340\u2013351. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-52513-0_18"},{"doi-asserted-by":"crossref","unstructured":"Yan, F., Foster, S., Habli, I.: Automated compositional verification for robotic state machines using Isabelle\/HOL. In: 27th International Conference on Engineering of Complex Computer Systems (ICECCS). IEEE (2023)","key":"2_CR121","DOI":"10.1109\/ICECCS59891.2023.00029"},{"key":"2_CR122","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"404","DOI":"10.1007\/978-3-031-17244-1_24","volume-title":"Formal Methods and Software Engineering","author":"K Ye","year":"2022","unstructured":"Ye, K., Foster, S., Woodcock, J.: Formally verified animation for RoboChart using interaction trees. In: Riesco, A., Zhang, M. (eds.) ICFEM 2022. LNCS, vol. 13478, pp. 404\u2013420. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-17244-1_24"},{"unstructured":"Zeyda, F., Cavalcanti, A.L.C.: Circus model for the SCJ framework. Technical report, University of York, Department of Computer Science, York, UK (2012)","key":"2_CR123"},{"key":"2_CR124","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/978-3-319-52228-9_8","volume-title":"Unifying Theories of Programming","author":"F Zeyda","year":"2017","unstructured":"Zeyda, F., Foster, S., Freitas, L.: An axiomatic value model for Isabelle\/UTP. In: Bowen, J.P., Zhu, H. (eds.) UTP 2016. LNCS, vol. 10134, pp. 155\u2013175. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52228-9_8"}],"container-title":["Lecture Notes in Computer Science","Theories of Programming and Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-40436-8_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,12,21]],"date-time":"2023-12-21T09:34:09Z","timestamp":1703151249000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40436-8_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031404351","9783031404368"],"references-count":124,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40436-8_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"8 September 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}