{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,2]],"date-time":"2025-07-02T11:33:23Z","timestamp":1751456003763,"version":"3.40.3"},"publisher-location":"Cham","reference-count":80,"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_1","type":"book-chapter","created":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:04:03Z","timestamp":1694127843000},"page":"3-18","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Jifeng He at Oxford and Beyond: An Appreciation"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8748-6140","authenticated-orcid":false,"given":"Jonathan P.","family":"Bowen","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0214-8565","authenticated-orcid":false,"given":"Huibiao","family":"Zhu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,9,8]]},"reference":[{"key":"1_CR1","unstructured":"Bj\u00f8rner, D., et al.: A ProCoS project description: ESPRIT BRA 3104. Bull. Eur. Assoc. Theor. Comput. Sci. 39, 60\u201373 (1989). http:\/\/researchgate.net\/publication\/256643262"},{"key":"1_CR2","unstructured":"Bowen, J.P. (ed.): Towards Verified Systems, Real-Time Safety Critical Systems, vol. 2. Elsevier, Amsterdam (1994)"},{"key":"1_CR3","doi-asserted-by":"publisher","unstructured":"Bowen, J.P.: A relational approach to an algebraic community: from Paul Erd\u0151s to He Jifeng. In: Liu et al. [58], pp. 54\u201366. https:\/\/doi.org\/10.1007\/978-3-642-39698-4_4","DOI":"10.1007\/978-3-642-39698-4_4"},{"key":"1_CR4","doi-asserted-by":"publisher","unstructured":"Bowen, J.P.: A personal formal methods archive. ResearchGate (2019). https:\/\/doi.org\/10.13140\/RG.2.2.31943.65447","DOI":"10.13140\/RG.2.2.31943.65447"},{"key":"1_CR5","unstructured":"Bowen, J.P.: FACS events, 2018\u20132020. FACS FACTS 2020(1), 7\u201321 (2020). https:\/\/www.bcs.org\/media\/5204\/facs-dec19.pdf"},{"issue":"3\u20134","key":"1_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3560267","volume":"34","author":"JP Bowen","year":"2022","unstructured":"Bowen, J.P.: Review on theories of programming: the life and works of tony Hoare. Form. Aspects Comput. 34(3\u20134), 1\u20133 (2022). https:\/\/doi.org\/10.1145\/3560267","journal-title":"Form. Aspects Comput."},{"issue":"5\u20136","key":"1_CR7","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0950-5849(95)99362-Q","volume":"37","author":"JP Bowen","year":"1995","unstructured":"Bowen, J.P., Gordon, M.J.C.: A shallow embedding of Z in HOL. Inf. Softw. Technol. 37(5\u20136), 269\u2013276 (1995). https:\/\/doi.org\/10.1016\/0950-5849(95)99362-Q","journal-title":"Inf. Softw. Technol."},{"issue":"1","key":"1_CR8","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1011184310224","volume":"19","author":"JP Bowen","year":"2001","unstructured":"Bowen, J.P., He, J.: An approach to the specification and verification of a hardware compilation scheme. J. Supercomput. 19(1), 23\u201339 (2001). https:\/\/doi.org\/10.1023\/A:1011184310224","journal-title":"J. Supercomput."},{"key":"1_CR9","doi-asserted-by":"publisher","unstructured":"Bowen, J.P., He, J.: An algebraic approach to hardware compilation. In: Gabbar, H.A. (ed.) Modern Formal Methods and Applications, pp. 151\u2013176. Springer, Dordrecht (2006). https:\/\/doi.org\/10.1007\/1-4020-4223-X_7","DOI":"10.1007\/1-4020-4223-X_7"},{"key":"1_CR10","unstructured":"Bowen, J.P., He, J., Hale, R.W.S., Herbert, J.M.J.: Towards verified systems: the SAFEMOS project. In: Mitchell, C., Stavridou, V. (eds.) Mathematics of Dependable Systems, Institute of Mathematics and Its Applications Conference Series, vol. 55, pp. 23\u201348. Oxford University Press (1995). http:\/\/researchgate.net\/publication\/2525857"},{"key":"1_CR11","doi-asserted-by":"publisher","unstructured":"Bowen, J.P., He, J., Page, I.: Hardware compilation. In: Bowen [2], chap. 10, pp. 193\u2013207. https:\/\/doi.org\/10.1016\/B978-0-444-89901-9.50019-7","DOI":"10.1016\/B978-0-444-89901-9.50019-7"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BFb0024175","volume-title":"Programming Language Implementation and Logic Programming","author":"JP Bowen","year":"1990","unstructured":"Bowen, J.P., He, J., Pandya, P.K.: An approach to verifiable compiling specification and prototyping. In: Deransart, P., Maluszy\u0144ski, J. (eds.) PLILP 1990. LNCS, vol. 456, pp. 45\u201359. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/BFb0024175"},{"key":"1_CR13","doi-asserted-by":"publisher","unstructured":"Bowen, J.P., He, J., Xu, Q.: An animatable operational semantics of the Verilog hardware description language. In: ICFEM 2000: Third IEEE International Conference on Formal Engineering Methods, pp. 199\u2013207. IEEE (2000). https:\/\/doi.org\/10.1109\/ICFEM.2000.873820","DOI":"10.1109\/ICFEM.2000.873820"},{"key":"1_CR14","unstructured":"Bowen, J.P., et al.: Provably correct systems \u2013 FTRTFT\u201994 tutorial. In: Third International School and Symposium, Formal Techniques in Real Time and Fault Tolerant Systems. No. [COORD JB 7\/1] in ProCoS document, Christian-Albrechts-Universit\u00e4t, L\u00fcbeck, Germany, September 1994. http:\/\/researchgate.net\/publication\/2420842, School Material"},{"key":"1_CR15","unstructured":"Bowen, J.P., Hoare, C.A.R., Langmaack, H., Olderog, E.R., Ravn, A.P.: A ProCoS II project final report: ESPRIT basic research project 7071. Bull. Eur. Assoc. Theor. Comput. Sci. 59, 76\u201399 (1996). http:\/\/researchgate.net\/publication\/2255515"},{"key":"1_CR16","unstructured":"Bowen, J.P., Hoare, C.A.R., Langmaack, H., Olderog, E.R., Ravn, A.P.: A ProCoS-WG working group final report: ESPRIT working group 8694. Bull. Eur. Assoc. Theor. Comput. Sci. 64, 63\u201372 (1998). http:\/\/researchgate.net\/publication\/2527052"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-52228-9","volume-title":"Unifying Theories of Programming","year":"2017","unstructured":"Bowen, J.P., Zhu, H. (eds.): UTP 2016. LNCS, vol. 10134. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52228-9"},{"key":"1_CR18","doi-asserted-by":"publisher","unstructured":"Bowen, J.P., Li, Q., Xu, Q. (eds.): Theories of Programming and Formal Methods: Essays Dedicated to Jifeng He on the Occasion of His 80th Birthday, LNCS, vol. 14080. Springer, Berlin, Heidelberg (2023). https:\/\/doi.org\/10.1007\/978-3-031-40436-8","DOI":"10.1007\/978-3-031-40436-8"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Hale, R.W.S., He, J.: A real-time programming language. In: Bowen, J.P. (ed.) Towards Verified Systems, Real-Time Safety Critical Systems, vol. 2, chap. 6, pp. 115\u2013130. Elsevier (1994)","DOI":"10.1016\/B978-0-444-89901-9.50015-X"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1007\/3-540-57182-5_45","volume-title":"Mathematical Foundations of Computer Science 1993","author":"J He","year":"1993","unstructured":"He, J.: Hybrid parallel programming and implementation of synchronised communication. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 537\u2013546. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_45"},{"key":"1_CR21","unstructured":"He, J.: Provably Correct Systems: Modelling of Communication Languages and Design of Optimized Compilers. International Series in Software Engineering. McGraw-Hill, New York (1994)"},{"key":"1_CR22","doi-asserted-by":"publisher","unstructured":"He, J.: A new roadmap for linking theories of programming. In: Bowen and Zhu [17], pp. 26\u201343. https:\/\/doi.org\/10.1007\/978-3-319-52228-9_2","DOI":"10.1007\/978-3-319-52228-9_2"},{"key":"1_CR23","unstructured":"He, J., Bowen, J.P.: Compiling specification for ProCoS language PLR$$_0$$. ProCoS document [OU HJF 6], Oxford University Computing Laboratory (1991). http:\/\/researchgate.net\/publication\/319069362"},{"key":"1_CR24","doi-asserted-by":"publisher","unstructured":"He, J., Bowen, J.P.: Time interval semantics and implementation of a real-time programming language. In: Fourth Euromicro Workshop on Real-Time Systems, pp. 110\u2013115. IEEE (1992). https:\/\/doi.org\/10.1109\/EMWRT.1992.637480","DOI":"10.1109\/EMWRT.1992.637480"},{"issue":"6","key":"1_CR25","doi-asserted-by":"publisher","first-page":"643","DOI":"10.1007\/BF03259390","volume":"6","author":"J He","year":"1994","unstructured":"He, J., Bowen, J.P.: Specification, verification and prototyping of an optimized compiler. Form. Aspects Comput. 6(6), 643\u2013658 (1994). https:\/\/doi.org\/10.1007\/BF03259390","journal-title":"Form. Aspects Comput."},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/0020-0190(93)90219-Y","volume":"45","author":"J He","year":"1993","unstructured":"He, J., Hoare, C.A.R.: From algebra to operational semantics. Inf. Process. Lett. 45, 75\u201380 (1993). https:\/\/doi.org\/10.1016\/0020-0190(93)90219-Y","journal-title":"Inf. Process. Lett."},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/3-540-16442-1_14","volume-title":"ESOP 86","author":"J He","year":"1986","unstructured":"He, J., Hoare, C.A.R., Sanders, J.W.: Data refinement refined resume. In: Robinet, B., Wilhelm, R. (eds.) ESOP 1986. LNCS, vol. 213, pp. 187\u2013196. Springer, Heidelberg (1986). https:\/\/doi.org\/10.1007\/3-540-16442-1_14"},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/BFb0021726","volume-title":"Correct Hardware Design and Verification Methods","author":"J He","year":"1993","unstructured":"He, J., Page, I., Bowen, J.P.: Towards a provably correct hardware implementation of Occam. In: Milne, G.J., Pierre, L. (eds.) CHARME 1993. LNCS, vol. 683, pp. 214\u2013225. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/BFb0021726"},{"key":"1_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/978-3-642-14521-6_2","volume-title":"Unifying Theories of Programming","author":"J He","year":"2010","unstructured":"He, J.: Transaction calculus. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 2\u201321. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14521-6_2"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/11768173_3","volume-title":"Unifying Theories of Programming","author":"J He","year":"2006","unstructured":"He, J., Hoare, C.A.R.: CSP is a retract of CCS. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 38\u201362. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11768173_3"},{"issue":"11\u201313","key":"1_CR31","doi-asserted-by":"publisher","first-page":"1311","DOI":"10.1016\/j.tcs.2009.12.012","volume":"411","author":"J He","year":"2010","unstructured":"He, J., Hoare, C.A.R.: CSP is a retract of CCS. Theor. Comput. Sci. 411(11\u201313), 1311\u20131337 (2010). https:\/\/doi.org\/10.1016\/j.tcs.2009.12.012","journal-title":"Theor. Comput. Sci."},{"key":"1_CR32","doi-asserted-by":"crossref","unstructured":"He, J., Hoare, C.A.R.: Unifying theories of programming. In: RelMiCS: 4th International Seminar on Relational Methods in Computer Science, pp. 97\u201399. Warsaw, Poland, September 1998","DOI":"10.1007\/BFb0002714"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"124","DOI":"10.1007\/978-3-319-51046-0_7","volume-title":"Concurrency, Security, and Puzzles","author":"J He","year":"2017","unstructured":"He, J., Li, Q.: A hybrid relational modelling language. In: Gibson-Robinson, T., Hopcroft, P., Lazi\u0107, R. (eds.) Concurrency, Security, and Puzzles. LNCS, vol. 10160, pp. 124\u2013143. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-51046-0_7"},{"key":"1_CR34","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.scico.2017.10.009","volume":"162","author":"J He","year":"2018","unstructured":"He, J., Li, Q.: A new roadmap for linking theories of programming and its applications on GCL and CSP. Sci. Comput. Program. 162, 3\u201334 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.10.009","journal-title":"Sci. Comput. Program."},{"issue":"1\u20132","key":"1_CR35","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.tcs.2006.07.034","volume":"365","author":"J He","year":"2006","unstructured":"He, J., Li, X., Liu, Z.: rCOS: a refinement calculus of object systems. Theor. Comput. Sci. 365(1\u20132), 109\u2013142 (2006). https:\/\/doi.org\/10.1016\/j.tcs.2006.07.034","journal-title":"Theor. Comput. Sci."},{"key":"1_CR36","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. Sci. Comput. Program. 28, 171\u2013192 (1997)","journal-title":"Sci. Comput. Program."},{"key":"1_CR37","unstructured":"He, J., Xu, Q.: An operational semantics of a simulator algorithm. In: Arabnia, H.R. (ed.) Proceedings of the International Conference on Parallel and Distributed Processing Techniques and Applications, PDPTA 2000, 24\u201329 June 2000, Las Vegas, Nevada, USA. CSREA Press (2000)"},{"issue":"1","key":"1_CR38","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/s001650300001","volume":"15","author":"J He","year":"2003","unstructured":"He, J., Xu, Q.: Advanced features of Duration Calculus and their applications in sequential hybrid programs. Form. Aspects Comput. 15(1), 84\u201399 (2003). https:\/\/doi.org\/10.1007\/s001650300001","journal-title":"Form. Aspects Comput."},{"key":"1_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1007\/3-540-58468-4_172","volume-title":"Formal Techniques in Real-Time and Fault-Tolerant Systems","author":"J He","year":"1994","unstructured":"He, J., Zheng, J.: Simulation approach to provably correct hardware compilation. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT ProCoS 1994. LNCS, vol. 863, pp. 336\u2013350. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58468-4_172"},{"key":"1_CR40","doi-asserted-by":"publisher","unstructured":"He, J., Zhu, H.: Formalising VERILOG. In: Proceedings of the 2000 7th IEEE International Conference on Electronics, Circuits and Systems, ICECS 2000, Jounieh, Lebanon, 17\u201320 December 2000, pp. 412\u2013415. IEEE (2000). https:\/\/doi.org\/10.1109\/ICECS.2000.911568","DOI":"10.1109\/ICECS.2000.911568"},{"issue":"1","key":"1_CR41","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s11704-007-0002-7","volume":"1","author":"J He","year":"2007","unstructured":"He, J., Zhu, H., Pu, G.: A model for BPEL-like languages. Front. Comput. Sci. China 1(1), 9\u201319 (2007). https:\/\/doi.org\/10.1007\/s11704-007-0002-7","journal-title":"Front. Comput. Sci. China"},{"key":"1_CR42","unstructured":"Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science, Prentice Hall, Hoboken (1985)"},{"key":"1_CR43","unstructured":"Hoare, C.A.R.: Recommendation letter (2002). Private communication via K. He (May 2023)"},{"key":"1_CR44","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification. Technical Monograph PRG-44, Oxford University Computing Laboratory, Programming Research Group, Oxford, UK, June 1985"},{"issue":"1","key":"1_CR45","doi-asserted-by":"publisher","first-page":"51","DOI":"10.3233\/FI-1986-9104","volume":"9","author":"CAR Hoare","year":"1986","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification: Part I. Fund. Inform. 9(1), 51\u201384 (1986). https:\/\/doi.org\/10.3233\/FI-1986-9104","journal-title":"Fund. Inform."},{"issue":"2","key":"1_CR46","doi-asserted-by":"publisher","first-page":"217","DOI":"10.3233\/FI-1986-9205","volume":"9","author":"CAR Hoare","year":"1986","unstructured":"Hoare, C.A.R., He, J.: The weakest prespecification: Part II. Fund. Inform. 9(2), 217\u2013251 (1986). https:\/\/doi.org\/10.3233\/FI-1986-9205","journal-title":"Fund. Inform."},{"key":"1_CR47","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R., He, J., Bowen, J.P., Pandya, P.: An algebraic approach to verifiable compiling specification and prototyping of the ProCoS level 0 programming language. In: Directorate-General XIII of the Commission of the European Communities (ed.) ESPRIT \u201990 Conference, pp. 804\u2013818. Kluwer Academic Publishers (1990). https:\/\/doi.org\/10.1007\/978-94-009-0705-8_65","DOI":"10.1007\/978-94-009-0705-8_65"},{"issue":"2","key":"1_CR48","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1016\/0020-0190(87)90224-9","volume":"25","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., He, J., Sanders, J.W.: Prespecification in data refinement. Inf. Process. Lett. 25(2), 71\u201376 (1987). https:\/\/doi.org\/10.1016\/0020-0190(87)90224-9","journal-title":"Inf. Process. Lett."},{"key":"1_CR49","unstructured":"Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science, Prentice Hall, Hoboken (1998)"},{"issue":"8","key":"1_CR50","doi-asserted-by":"publisher","first-page":"701","DOI":"10.1007\/BF01191809","volume":"30","author":"CAR Hoare","year":"1993","unstructured":"Hoare, C.A.R., He, J., Sampaio, A.: Normal form approach to compiler design. Acta Informatica 30(8), 701\u2013739 (1993). https:\/\/doi.org\/10.1007\/BF01191809","journal-title":"Acta Informatica"},{"issue":"8","key":"1_CR51","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/27651.27653","volume":"30","author":"CAR Hoare","year":"1987","unstructured":"Hoare, C.A.R., et al.: Laws of programming. Commun. ACM 30(8), 672\u2013686 (1987)","journal-title":"Commun. ACM"},{"key":"1_CR52","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, 127\u2013132 (1987). https:\/\/doi.org\/10.1016\/0020-0190(87)90106-2","journal-title":"Inf. Process. Lett."},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-48743-3_1","volume-title":"ECOOP\u2019 99 \u2014 Object-Oriented Programming","author":"CAR Hoare","year":"1999","unstructured":"Hoare, C.A.R., He, J.: A trace model for pointers and objects. In: Guerraoui, Rachid (ed.) ECOOP 1999. LNCS, vol. 1628, pp. 1\u201318. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48743-3_1"},{"key":"1_CR54","doi-asserted-by":"publisher","unstructured":"Jones, C.: List of Tony Hoare\u2019s publications. In: Jones and Misra [55], pp. 394\u2013315. https:\/\/doi.org\/10.1145\/3477355.3477375, Appendix D","DOI":"10.1145\/3477355.3477375"},{"key":"1_CR55","doi-asserted-by":"publisher","unstructured":"Jones, C.B., Misra, J. (eds.): Theories of Programming: The Life and Works of Tony Hoare, ACM Books, vol. 39. Association for Computing Machinery (2021). https:\/\/doi.org\/10.1145\/3477355","DOI":"10.1145\/3477355"},{"key":"1_CR56","doi-asserted-by":"publisher","unstructured":"Li, X., Liu, Z., He, J.: A formal semantics of UML sequence diagram. In: Proceedings of the Australian Software Engineering Conference (ASWEC), pp. 168\u2013177. IEEE (2004). https:\/\/doi.org\/10.1109\/ASWEC.2004.1290469","DOI":"10.1109\/ASWEC.2004.1290469"},{"key":"1_CR57","unstructured":"Li, Y., He, J.: Formalising Verilog: operational semantics and bisimulation. Technical report 217, UNU\/IIST, P.O. Box 3058, Macau SAR, China, November 2000"},{"key":"1_CR58","doi-asserted-by":"publisher","unstructured":"Liu, Z., Woodcock, J.C.P., Zhu, H. (eds.): Theories of Programming and Formal Methods, LNCS, vol. 8051. Springer, Berlin, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39698-4","DOI":"10.1007\/978-3-642-39698-4"},{"key":"1_CR59","doi-asserted-by":"publisher","unstructured":"Liu, Z.: Linking formal methods in software development \u2013 a reflection on the development of rCOS. In: Bowen et al. [18], this volume. https:\/\/doi.org\/10.1007\/978-3-031-40436-8_3","DOI":"10.1007\/978-3-031-40436-8_3"},{"key":"1_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/11561163_9","volume-title":"Formal Methods for Components and Objects","author":"Z Liu","year":"2005","unstructured":"Liu, Z., He, J., Li, X.: rCOS: refinement of component and object systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 183\u2013221. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11561163_9"},{"key":"1_CR61","doi-asserted-by":"publisher","unstructured":"Milner, R.: A Calculus of Communicating Systems. Springer, Heidelberg (1980). https:\/\/doi.org\/10.1007\/3-540-10235-3_11","DOI":"10.1007\/3-540-10235-3_11"},{"key":"1_CR62","doi-asserted-by":"publisher","unstructured":"M\u00f6ller, B., Hoare, C.A.R., M\u00fcller, M.E., Struth, G.: A discrete geometric model of concurrent program execution. In: Bowen and Zhu [17], pp. 1\u201325. https:\/\/doi.org\/10.1007\/978-3-319-52228-9_1","DOI":"10.1007\/978-3-319-52228-9_1"},{"key":"1_CR63","doi-asserted-by":"publisher","unstructured":"Mu, R., Li, Q.: A Coq implementation of the program algebra in Jifeng He\u2019s new roadmap for linking theories of programming. In: Bowen et al. [18], this volume. https:\/\/doi.org\/10.1007\/978-3-031-40436-8_15","DOI":"10.1007\/978-3-031-40436-8_15"},{"key":"1_CR64","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/3-540-58027-1_11","volume-title":"Mathematical Foundations of Programming Semantics","author":"D Scholefield","year":"1994","unstructured":"Scholefield, D., Zedan, H., He, J.: A predicative semantics for the refinement of real-time systems. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 230\u2013249. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/3-540-58027-1_11"},{"key":"1_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/3-540-57182-5_60","volume-title":"Mathematical Foundations of Computer Science 1993","author":"D Scholefield","year":"1993","unstructured":"Scholefield, D., Zedan, H., He, J.: Real-time refinement: semantics and application. In: Borzyszkowski, A.M., Soko\u0142owski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 693\u2013702. Springer, Heidelberg (1993). https:\/\/doi.org\/10.1007\/3-540-57182-5_60"},{"key":"1_CR66","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1016\/0304-3975(94)90096-5","volume":"131","author":"D Scolefield","year":"1994","unstructured":"Scolefield, D., Zedan, H., He, J.: A specification-oriented semantics for the refinement of real-time systems. Theor. Comput. Sci. 131, 219\u2013241 (1994)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR67","doi-asserted-by":"publisher","unstructured":"Sheng, F., Zhu, H., He, J., Yang, Z., Bowen, J.P.: Theoretical and practical aspects of linking operational and algebraic semantics for MDESL. ACM Trans. Softw. Eng. Methodol. 28(3), 14:1\u201314:46 (2019). https:\/\/doi.org\/10.1145\/3295699","DOI":"10.1145\/3295699"},{"issue":"2\u20133","key":"1_CR68","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/s00165-020-00513-4","volume":"32","author":"F Sheng","year":"2020","unstructured":"Sheng, F., Zhu, H., He, J., Yang, Z., Bowen, J.P.: Theoretical and practical approaches to the denotational semantics for MDESL based on UTP. Form. Aspects Comput. 32(2\u20133), 275\u2013314 (2020). https:\/\/doi.org\/10.1007\/s00165-020-00513-4","journal-title":"Form. Aspects Comput."},{"key":"1_CR69","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s00165-009-0119-6","volume":"22","author":"A Sherif","year":"2010","unstructured":"Sherif, A., Cavalcanti, A., He, J., Sampaio, A.: A process algebraic framework forspecification and validation of real-time systems. Form. Aspects Comput. 22, 153\u2013191 (2010). https:\/\/doi.org\/10.1007\/s00165-009-0119-6","journal-title":"Form. Aspects Comput."},{"key":"1_CR70","doi-asserted-by":"publisher","unstructured":"Woodcock, J.: Hoare and He\u2019s unifying theories of programming. In: Jones and Misra [55], chap.\u00a013, pp. 287\u2013315. https:\/\/doi.org\/10.1145\/3477355.3477369","DOI":"10.1145\/3477355.3477369"},{"key":"1_CR71","doi-asserted-by":"publisher","unstructured":"Woodcock, J., Cavalcanti, A., Foster, S., Oliveira, M., Sampaio, A., Zeyda, F.: UTP, Circus, and Isabelle. In: Bowen et al. [18], this volume. https:\/\/doi.org\/10.1007\/978-3-031-40436-8_2","DOI":"10.1007\/978-3-031-40436-8_2"},{"issue":"2","key":"1_CR72","doi-asserted-by":"publisher","first-page":"149","DOI":"10.1007\/BF01211617","volume":"9","author":"Q Xu","year":"1997","unstructured":"Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Form. Aspects Comput. 9(2), 149\u2013174 (1997). https:\/\/doi.org\/10.1007\/BF01211617","journal-title":"Form. Aspects Comput."},{"issue":"5","key":"1_CR73","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1016\/0020-0190(91)90122-X","volume":"40","author":"C Zhou","year":"1991","unstructured":"Zhou, C., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269\u2013276 (1991)","journal-title":"Inf. Process. Lett."},{"key":"1_CR74","doi-asserted-by":"publisher","unstructured":"Zhu, H., Bowen, J.P., He, J.: Deriving operational semantics from denotational semantics for Verilog. In: APSEC 2001: Eighth Asia-Pacific Software Engineering Conference, pp. 177\u2013184. IEEE (2001). https:\/\/doi.org\/10.1109\/APSEC.2001.991475","DOI":"10.1109\/APSEC.2001.991475"},{"key":"1_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"449","DOI":"10.1007\/3-540-44798-9_34","volume-title":"Correct Hardware Design and Verification Methods","author":"H Zhu","year":"2001","unstructured":"Zhu, H., Bowen, J.P., He, J.: From operational semantics to denotational semantics for Verilog. In: Margaria, T., Melham, T. (eds.) CHARME 2001. LNCS, vol. 2144, pp. 449\u2013464. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44798-9_34"},{"key":"1_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"600","DOI":"10.1007\/3-540-36103-0_61","volume-title":"Formal Methods and Software Engineering","author":"H Zhu","year":"2002","unstructured":"Zhu, H., Bowen, J.P., He, J.: Soundness, completeness and non-redundancy of operational semantics for Verilog based on denotational semantics. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 600\u2013612. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36103-0_61"},{"key":"1_CR77","unstructured":"Zhu, H., He, J.: A semantics of Verilog using duration calculus. In: Proceedings of the International Conference on Software: Theory and Practice, pp. 421\u2013432 (August 2000)"},{"key":"1_CR78","doi-asserted-by":"publisher","unstructured":"Zhu, H., He, J., Li, J., Bowen, J.P.: Algebraic approach to linking the semantics of web services. In: Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 10\u201314 September 2007, London, England, UK, pp. 315\u2013328. IEEE Computer Society (2007). https:\/\/doi.org\/10.1109\/SEFM.2007.4","DOI":"10.1109\/SEFM.2007.4"},{"issue":"3","key":"1_CR79","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s11334-011-0172-1","volume":"7","author":"H Zhu","year":"2011","unstructured":"Zhu, H., He, J., Li, J., Bowen, J.P.: Algebraic approach to linking the semantics of web services. Innov. Syst. Softw. Eng. 7(3), 209\u2013224 (2011). https:\/\/doi.org\/10.1007\/s11334-011-0172-1","journal-title":"Innov. Syst. Softw. Eng."},{"issue":"4","key":"1_CR80","doi-asserted-by":"publisher","first-page":"283","DOI":"10.1007\/s11334-010-0134-z","volume":"6","author":"H Zhu","year":"2010","unstructured":"Zhu, H., He, J., Li, J., Pu, G., Bowen, J.P.: Linking denotational semantics with operational semantics for web services. Innov. Syst. Softw. Eng. 6(4), 283\u2013298 (2010). https:\/\/doi.org\/10.1007\/s11334-010-0134-z","journal-title":"Innov. Syst. Softw. Eng."}],"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_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,7]],"date-time":"2023-09-07T23:04:43Z","timestamp":1694127883000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-40436-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031404351","9783031404368"],"references-count":80,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-40436-8_1","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"}}]}}