{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:14:43Z","timestamp":1750220083770,"version":"3.41.0"},"reference-count":104,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2022,3,31]],"date-time":"2022-03-31T00:00:00Z","timestamp":1648684800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"Leverhulme Foundation","award":["RPG-2019-020"],"award-info":[{"award-number":["RPG-2019-020"]}]},{"name":"EPSRC Strata Platform"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2022,3,31]]},"abstract":"<jats:p>In addition to the major UK contributions to research underpinning formal approaches to the specification and development of computer systems\u2014and perhaps as a consequence of this\u2014some significant attempts to deploy the ideas into practical environments have taken place in the United Kingdom. The authors of this article have been involved in formal methods for many years and both had contact with a significant proportion of this history. This article both lists key ideas and indicates where attempts were made to use the ideas in practice. Not all of these deployment stories have been a complete success and an attempt is made to tease out lessons that influence the probability of successful long-term changes to software engineering.<\/jats:p>","DOI":"10.1145\/3522577","type":"journal-article","created":{"date-parts":[[2022,3,23]],"date-time":"2022-03-23T14:38:14Z","timestamp":1648046294000},"page":"1-21","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["The Development and Deployment of Formal Methods in the UK"],"prefix":"10.1145","volume":"34","author":[{"given":"Cliff B.","family":"Jones","sequence":"first","affiliation":[{"name":"School of Computing, Newcastle University, Newcastle upon Tyne, UK"}]},{"given":"Martyn","family":"Thomas","sequence":"additional","affiliation":[{"name":"Emeritus Professor of IT, Gresham College, London, UK"}]}],"member":"320","published-online":{"date-parts":[[2022,7,5]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.5555\/236705"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.5555\/1855020"},{"key":"e_1_3_2_4_2","volume-title":"The Event-B Book","author":"Abrial J.-R.","year":"2010","unstructured":"J.-R. Abrial. 2010. The Event-B Book. Cambridge University Press, Cambridge, UK."},{"key":"e_1_3_2_5_2","first-page":"24","article-title":"Correctness by construction: Better can also be cheaper","volume":"2","author":"Amey Peter","year":"2002","unstructured":"Peter Amey. 2002. Correctness by construction: Better can also be cheaper. CrossTalk: the Journal of Defense Software Engineering 2 (3 2002), 24\u201328.","journal-title":"CrossTalk: the Journal of Defense Software Engineering"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00501-3"},{"key":"e_1_3_2_7_2","volume-title":"Formalising Meaning: a History of Programming Language Semantics","author":"Astarte Troy K.","year":"2019","unstructured":"Troy K. Astarte. 2019. Formalising Meaning: a History of Programming Language Semantics. Ph.D. Dissertation. Newcastle University."},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-54997-8"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01386216"},{"key":"e_1_3_2_11_2","volume-title":"Proceedings of IEEE International Symposium on Secure Software Engineering","author":"Barnes J.","year":"2006","unstructured":"J. Barnes, R. Johnson, J. C. Widmaier, B. Everett, R. Chapman, and Cooper D.2006. Engineering the Tokeneer enclave protection software. In Proceedings of IEEE International Symposium on Secure Software Engineering, S. Redwine, Hall A., and J. Wing (Eds.). IEEE Computer Society."},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1147\/rd.276.0558"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/b138838"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-08766-4"},{"key":"e_1_3_2_15_2","volume-title":"Formal Specification and Software Development","author":"Bj\u00f8rner Dines","year":"1982","unstructured":"Dines Bj\u00f8rner and Cliff B. Jones (Eds.). 1982. Formal Specification and Software Development. Prentice Hall International. Retrieved from http:\/\/homepages.cs.ncl.ac.uk\/cliff.jones\/ftp-stuff\/BjornerJones1982."},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17654-3"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477355"},{"key":"e_1_3_2_18_2","first-page":"214","volume-title":"Proceedings of the FME\u201996: International Symposium of Formal Methods Europe (Lecture Notes in Computer Science)","volume":"1051","author":"Brookes T. M.","year":"1996","unstructured":"T. M. Brookes, John S. Fitzgerald, and Peter Gorm Larsen. 1996. Formal and informal specifications of a secure system component: Final results in a comparative study. In Proceedings of the FME\u201996: International Symposium of Formal Methods Europe (Lecture Notes in Computer Science), Vol. 1051. Springer-Verlag, 214\u2013227."},{"issue":"7","key":"e_1_3_2_19_2","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1109\/MAHC.1985.10001","article-title":"Christopher Strachey, 1916-1975: A biographical note","volume":"1","author":"Campbell-Kelly Martin","year":"1985","unstructured":"Martin Campbell-Kelly. 1985. Christopher Strachey, 1916-1975: A biographical note. IEEE Annals of the History of Computing 1, 7 (1985), 19\u201342.","journal-title":"IEEE Annals of the History of Computing"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-05089-3","volume-title":"FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009, Proceedings","volume":"5850","author":"Cavalcanti Ana","year":"2009","unstructured":"Ana Cavalcanti and Dennis Dams (Eds.). 2009. FM 2009: Formal Methods: Second World Congress, Eindhoven, The Netherlands, November 2\u20136, 2009, Proceedings. Vol. 5850. Springer."},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-66494-7_9"},{"key":"e_1_3_2_22_2","doi-asserted-by":"crossref","first-page":"17","DOI":"10.1007\/978-3-319-08970-6_2","volume-title":"Proceedings of the Interactive Theorem Proving (Lecture Notes in Computer Science)","volume":"8558","author":"Chapman R.","year":"2014","unstructured":"R. Chapman and F. Schanda. 2014. Are we there yet? 20 years of industrial theorem proving with SPARK. In Proceedings of the Interactive Theorem Proving (Lecture Notes in Computer Science), G. Klein and R. Gamboa (Eds.), Vol. 8558. Springer-Verlag, 17\u201326."},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_2_24_2","doi-asserted-by":"crossref","first-page":"216","DOI":"10.1007\/3-540-48249-0_19","volume-title":"Proceedings of the International Conference on Computer Safety, Reliability, and Security","author":"Clement Tim","year":"1999","unstructured":"Tim Clement, Ian Cottam, Peter Froome, and Claire Jones. 1999. The development of a commercial \u201cshrink-wrapped application\u201d to safety integrity level 2: The DUST-EXPERT\u2122 story. In Proceedings of the International Conference on Computer Safety, Reliability, and Security. Springer-Verlag, 216\u2013225."},{"key":"e_1_3_2_25_2","volume-title":"Proceedings of the VLSI Specification, Verification and Synthesis","volume":"35","author":"Cohn A.","year":"1988","unstructured":"A. Cohn. 1988. A proof of correctness of the VIPER microprocessor: The first level. In Proceedings of the VLSI Specification, Verification and Synthesis, G. Birtwistle and P.A. Subrahmanyam (Eds.). Vol. 35. Kluwer."},{"key":"e_1_3_2_26_2","volume-title":"Introducing Formal Methods: The CICS Experience with Z","author":"Collins B. P.","year":"1987","unstructured":"B. P. Collins, J. E. Nicholls, and I. H. Sorensen. 1987. Introducing Formal Methods: The CICS Experience with Z. Technical Report TR12.060. IBM Hursley Laboratory."},{"key":"e_1_3_2_27_2","first-page":"38","volume-title":"Proceedings of the Computer Aided Verification. CAV 2018 (Lecture Notes in Computer Science)","volume":"10981","author":"Cook Byron","year":"2018","unstructured":"Byron Cook. 2018. Formal reasoning about the security of Amazon Web Services. In Proceedings of the Computer Aided Verification. CAV 2018 (Lecture Notes in Computer Science), Weissenbacher G. Chockler H. (Ed.), Vol. 10981. Springer-Verlag, 38\u201347."},{"key":"e_1_3_2_28_2","first-page":"26","volume-title":"Proceedings of the International Symposium of Formal Methods Europe (Lecture Notes in Computer Science)","volume":"873","author":"Dehbonei Babak","year":"1994","unstructured":"Babak Dehbonei and Fernando Mejia. 1994. Formal methods in the railways signalling industry. In Proceedings of the International Symposium of Formal Methods Europe (Lecture Notes in Computer Science), Vol. 873. Springer-Verlag, 26\u201334."},{"key":"e_1_3_2_29_2","unstructured":"Lecture Notes in Computer Science The Analysis of Concurrent Systems: Cambridge September 1983 Proceedings of a Workshop 207 B. T. Denvir W. T. Harwood M. I. Jackson M. J. Wray 1985"},{"key":"e_1_3_2_30_2","first-page":"16","article-title":"Fifty years of formal methods in software engineering","author":"Denvir T.","year":"2017","unstructured":"T. Denvir. 2017. Fifty years of formal methods in software engineering. FACTS (8 2017), 16\u201326. Retrieved from https:\/\/cdn.bcs.org\/bcs-org-media\/3080\/facs-aug17.pdf.","journal-title":"FACTS"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_2_32_2","volume-title":"Sizewell B Primary Protection System. An Assessment of the Confirmatory Review Processes","author":"Fenney T.","year":"1995","unstructured":"T. Fenney. 1995. Sizewell B Primary Protection System. An Assessment of the Confirmatory Review Processes. Technical Report. Nuclear Electric plc."},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.1145\/3357231"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09836-5"},{"key":"e_1_3_2_36_2","doi-asserted-by":"crossref","first-page":"169","DOI":"10.7551\/mitpress\/5641.003.0012","volume-title":"Proceedings of the Proof, Language, and Interaction","author":"Gordon Mike","year":"2000","unstructured":"Mike Gordon. 2000. From LCF to HOL: A short history. In Proceedings of the Proof, Language, and Interaction. 169\u2013186."},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.506463"},{"key":"e_1_3_2_39_2","first-page":"1","volume-title":"Proceedings of the Formal Methods and Software Engineering (Lecture Notes in Computer Science)","volume":"3785","author":"Hall Anthony","year":"2005","unstructured":"Anthony Hall. 2005. Realising the benefits of formal methods. In Proceedings of the Formal Methods and Software Engineering (Lecture Notes in Computer Science), Vol. 3785. Springer-Verlag, 1\u20134."},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.976937"},{"key":"e_1_3_2_41_2","first-page":"1","volume-title":"Proceedings of the 2018 IEEE 18th International Working Conference on Source Code Analysis and Manipulation","author":"Harman Mark","year":"2018","unstructured":"Mark Harman and Peter O\u2019Hearn. 2018. From start-ups to scale-ups: Opportunities and open problems for static and dynamic program analysis. In Proceedings of the 2018 IEEE 18th International Working Conference on Source Code Analysis and Manipulation. IEEE, 1\u201323."},{"key":"e_1_3_2_42_2","volume-title":"Specification Case Studies (second ed.)","author":"Hayes Ian","year":"1993","unstructured":"Ian Hayes (Ed.). 1993. Specification Case Studies (second ed.). Prentice Hall International, Englewood Cliffs, N.J."},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.5555\/102598"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/573859"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477355"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1145\/3378426"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_3_2_49_2","first-page":"74","volume-title":"Proceedings of the FME\u201996: Industrial Benefit and Advances in Formal Methods (Lecture Notes in Computer Science)","volume":"1051","author":"Hoare Jonathan","year":"1996","unstructured":"Jonathan Hoare, Jeremy Dick, Dave Neilson, and Ib S\u00f8rensen. 1996. Applying the B technologies to CICS. In Proceedings of the FME\u201996: Industrial Benefit and Advances in Formal Methods (Lecture Notes in Computer Science), M.-C. Gaudel and J. Woodcock (Eds.), Vol. 1051. Springer-Verlag, 74\u201384."},{"key":"e_1_3_2_50_2","first-page":"588","volume-title":"Proceedings of the VDM\u201991 Formal Software Development Methods (Lecture Notes in Computer Science)","volume":"551","author":"Houston Iain","year":"1991","unstructured":"Iain Houston and Steve King. 1991. CICS project report experiences and results from the use of Z in IBM. In Proceedings of the VDM\u201991 Formal Software Development Methods (Lecture Notes in Computer Science), S. Prehn and W. J. Toetenel (Eds.), Vol. 551. Springer-Verlag, 588\u2013596."},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.5555\/1095595"},{"key":"e_1_3_2_52_2","volume-title":"Problem Frames: Analyzing and Structuring Software Development Problems","author":"Jackson Michael","year":"2000","unstructured":"Michael Jackson. 2000. Problem Frames: Analyzing and Structuring Software Development Problems. Addison-Wesley."},{"key":"e_1_3_2_53_2","volume-title":"Proceedings of the Formal Methods and Software Development. TAPSOFT 1985 (Lecture Notes in Computer Science)","author":"Jackson M. I.","year":"1985","unstructured":"M. I. Jackson, B. T. Denvir, and R. C. Shaw. 1985. Experience of introducing the vienna development method into an industrial organisation. In Proceedings of the Formal Methods and Software Development. TAPSOFT 1985 (Lecture Notes in Computer Science), H. Ehrig, C. Floyd, M. Nivat, and J. Thatcher (Eds.). Springer-Verlag."},{"key":"e_1_3_2_54_2","volume-title":"Development of Correct Programs: An Example Based on Earley\u2019s Recogniser","author":"Jones C. B.","year":"1971","unstructured":"C. B. Jones. 1971. Development of Correct Programs: An Example Based on Earley\u2019s Recogniser. Technical Report TN 9000. IBM Laboratory, Hursley."},{"key":"e_1_3_2_55_2","volume-title":"Formal Development of Programs","author":"Jones C. B.","year":"1973","unstructured":"C. B. Jones. 1973. Formal Development of Programs. Technical Report 12.117. IBM Laboratory Hursley."},{"key":"e_1_3_2_56_2","volume-title":"Software Development: A Rigorous Approach","author":"Jones C. B.","year":"1980","unstructured":"C. B. Jones. 1980. Software Development: A Rigorous Approach. Prentice Hall International, Englewood Cliffs, N.J. Retrieved from http:\/\/portal.acm.org\/citation.cfm?id=539771."},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.3217\/jucs-007-08-0631"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/MAHC.2003.1203057"},{"key":"e_1_3_2_59_2","volume-title":"An Exegesis of Four Formal Descriptions of ALGOL 60","author":"Jones Cliff B.","year":"2016","unstructured":"Cliff B. Jones and Troy K. Astarte. 2016. An Exegesis of Four Formal Descriptions of ALGOL 60. Technical Report CS-TR-1498. Newcastle University School of Computer Science."},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-02928-9_6"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3180-9"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1145\/3477355"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.879807"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1016\/0066-4138(69)90005-6"},{"issue":"5","key":"e_1_3_2_65_2","first-page":"100","article-title":"Formal specification and verification of autonomous robotic systems: A survey","volume":"52","author":"Luckcuck Matt","year":"2019","unstructured":"Matt Luckcuck, Marie Farrell, Louise A. Dennis, Clare Dixon, and Michael Fisher. 2019. Formal specification and verification of autonomous robotic systems: A survey. Computing Surveys 52, 5 (2019), 100.","journal-title":"Computing Surveys"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/4529.001.0001"},{"key":"e_1_3_2_67_2","unstructured":"Marsh and O\u2019Neil. 1994. The Formal Semantics of SPARK. Praxis UK Bath England"},{"key":"e_1_3_2_68_2","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"H. ter Beek Maurice","year":"2019","unstructured":"ter Beek Maurice H.Annabelle McIver, and Jos\u00e9 Oliveira (Eds.). 2019. Formal Methods \u2013 The Next 30 Years. Lecture Notes in Computer Science, Vol. 11800. Springer-Verlag."},{"key":"e_1_3_2_69_2","first-page":"1","volume-title":"Proceedings of the Formal Language Description Languages for Computer Programming","author":"McCarthy John","year":"1966","unstructured":"John McCarthy. 1966. A formal description of a subset of ALGOL. In Proceedings of the Formal Language Description Languages for Computer Programming. North-Holland, 1\u201312."},{"key":"e_1_3_2_70_2","volume-title":"Z Guide for Beginners","author":"McMorran Mike","year":"1993","unstructured":"Mike McMorran and Steve Powell. 1993. Z Guide for Beginners. Alfred Waller Limited."},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01887200"},{"key":"e_1_3_2_72_2","volume-title":"Syntax and Semantics of VVSL: A Language for Structured VDM Specifications","author":"Middelburg C. A.","year":"1990","unstructured":"C. A. Middelburg. 1990. Syntax and Semantics of VVSL: A Language for Structured VDM Specifications. Ph.D. Dissertation. PTT Research, Leidschendam, Department of Applied Computer Science."},{"key":"e_1_3_2_73_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-10235-3"},{"key":"e_1_3_2_74_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00490-3"},{"key":"e_1_3_2_75_2","doi-asserted-by":"publisher","DOI":"10.5555\/184737"},{"key":"e_1_3_2_76_2","volume-title":"Ella 2000: A Language for Electronic System Design","author":"Morison J. D.","year":"1993","unstructured":"J. D. Morison and A. S. Clarke. 1993. Ella 2000: A Language for Electronic System Design. McGraw Hill."},{"key":"e_1_3_2_77_2","doi-asserted-by":"publisher","DOI":"10.5555\/82570"},{"key":"e_1_3_2_78_2","doi-asserted-by":"crossref","unstructured":"Peter O\u2019Hearn. 2015. From categorical logic to Facebook engineering. In Proceedings of the 2015 30th Annual ACM\/IEEE Symposium on Logic in Computer Science . IEEE 17\u201320.","DOI":"10.1109\/LICS.2015.11"},{"key":"e_1_3_2_79_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_80_2","doi-asserted-by":"crossref","unstructured":"Lawrence C. Paulson. 2018. Michael john caldwell gordon (FRS 1994) 28 February 1948\u201322 August 2017. (2018). Royal Society obituary.","DOI":"10.1098\/rsbm.2018.0019"},{"key":"e_1_3_2_81_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00492-1"},{"key":"e_1_3_2_82_2","volume-title":"Peirce on Signs: Writings on Semiotic","author":"Peirce Charles Sanders","year":"1991","unstructured":"Charles Sanders Peirce. 1991. Peirce on Signs: Writings on Semiotic. UNC Press Books."},{"key":"e_1_3_2_83_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.566148"},{"key":"e_1_3_2_84_2","volume-title":"A Structural Approach to Operational Semantics","author":"Plotkin G. D.","year":"1981","unstructured":"G. D. Plotkin. 1981. A Structural Approach to Operational Semantics. Technical Report DAIMI FN-19. Aarhus University."},{"key":"e_1_3_2_85_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.009"},{"key":"e_1_3_2_86_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.03.002"},{"key":"e_1_3_2_87_2","doi-asserted-by":"publisher","DOI":"10.5555\/2517722"},{"key":"e_1_3_2_88_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1977.229900"},{"key":"e_1_3_2_89_2","volume-title":"Proceedings of the Software Engineering Environments (Lecture Notes in Computer Science)","volume":"467","author":"Snowdon R. A.","year":"1990","unstructured":"R. A. Snowdon. 1990. An introduction to the IPSE 2.5 project. In Proceedings of the Software Engineering Environments (Lecture Notes in Computer Science), F. Long (Ed.), Vol. 467. Springer-Verlag."},{"key":"e_1_3_2_90_2","volume-title":"The Z Notation: A Reference Manual (second edition ed.)","author":"Spivey J. M.","year":"1992","unstructured":"J. M. Spivey. 1992. The Z Notation: A Reference Manual (second edition ed.). Prentice Hall International."},{"key":"e_1_3_2_91_2","doi-asserted-by":"publisher","DOI":"10.5555\/42447"},{"key":"e_1_3_2_92_2","doi-asserted-by":"publisher","DOI":"10.5555\/61690"},{"key":"e_1_3_2_93_2","volume-title":"Formal Language Description Languages for Computer Programming","author":"Steel T. B.","year":"1966","unstructured":"T. B. Steel (Ed.). 1966. Formal Language Description Languages for Computer Programming. North-Holland."},{"key":"e_1_3_2_94_2","article-title":"Spark: A successful contribution to the Lockheed C130-J Hercules II","author":"Systems Praxis Critical","year":"2006","unstructured":"Praxis Critical Systems. 2006. Spark: A successful contribution to the Lockheed C130-J Hercules II. Praxis report.","journal-title":"Praxis report"},{"key":"e_1_3_2_95_2","doi-asserted-by":"publisher","DOI":"10.1016\/0141-9331(93)90091-K"},{"key":"e_1_3_2_96_2","doi-asserted-by":"crossref","first-page":"171","DOI":"10.1007\/978-1-4471-2061-2_19","volume-title":"Proceedings of the International Conference on Computer Safety, Reliability and Security SAFECOMP\u201993","author":"Ward N. J.","year":"1993","unstructured":"N. J. Ward. 1993. The rigorous retrospective static analysis of the Sizewell \u2018B\u2019 Primary Protection System software. In Proceedings of the International Conference on Computer Safety, Reliability and Security SAFECOMP\u201993, G\u00f3rski J. (Ed.). Springer-Verlag, 171\u2013181."},{"key":"e_1_3_2_97_2","doi-asserted-by":"publisher","DOI":"10.1098\/rsta.2015.0402"},{"key":"e_1_3_2_98_2","series-title":"Lecture Notes in Computer Science","volume-title":"Formal Methods FM\u201999","author":"Wing J. M.","year":"1999","unstructured":"J. M. Wing, J. Woodcock, and J. Davies (Eds.). 1999. Formal Methods FM\u201999. Lecture Notes in Computer Science, Vol. 1709. Springer-Verlag."},{"key":"e_1_3_2_99_2","doi-asserted-by":"publisher","DOI":"10.1145\/359863.359883"},{"key":"e_1_3_2_100_2","doi-asserted-by":"crossref","first-page":"77","DOI":"10.1007\/978-1-4471-3203-5_4","volume-title":"Proceedings of the Z User Workshop, York 1991","author":"Woodcock J. C. P.","year":"1992","unstructured":"J. C. P. Woodcock and S. M. Brien. 1992. W: A logic for Z. In Proceedings of the Z User Workshop, York 1991. Springer-Verlag, Hard copy.77\u201396."},{"key":"e_1_3_2_101_2","volume-title":"Using Z: Specification, Refinement and Proof","author":"Woodcock Jim","year":"1996","unstructured":"Jim Woodcock and Jim Davies. 1996. Using Z: Specification, Refinement and Proof. Prentice Hall International."},{"key":"e_1_3_2_102_2","first-page":"405","volume-title":"Proceedings of the Reflections on the Work on","author":"Woodcock J.","year":"2010","unstructured":"J. Woodcock, E. G\u00f6kce Aydal, and R. Chapman. 2010. The Tokeneer experiments. In Proceedings of the Reflections on the Work on, Cliff B. Jones, A. W. Roscoe, and Kenneth R. Wood (Eds.). Springer-Verlag, 405\u2013430."},{"issue":"4","key":"e_1_3_2_103_2","doi-asserted-by":"crossref","DOI":"10.1145\/1592434.1592436","article-title":"Formal methods: Practice and experience","volume":"41","author":"Woodcock J.","year":"2009","unstructured":"J. Woodcock, P. G. Larsen, J. Bicarregui, and J. Fitzgerald. 2009. Formal methods: Practice and experience. Comput. Surveys 41, 4 (10 2009), 1\u201336.","journal-title":"Comput. Surveys"},{"key":"e_1_3_2_104_2","volume-title":"Guide to Algol 68 for users of RS Systems","author":"Woodward P. M.","year":"1983","unstructured":"P. M. Woodward and S. G. Bond. 1983. Guide to Algol 68 for users of RS Systems. Edward Arnold."},{"key":"e_1_3_2_105_2","doi-asserted-by":"publisher","DOI":"10.5555\/573467"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3522577","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3522577","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:09:33Z","timestamp":1750183773000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3522577"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,3,31]]},"references-count":104,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,3,31]]}},"alternative-id":["10.1145\/3522577"],"URL":"https:\/\/doi.org\/10.1145\/3522577","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2022,3,31]]},"assertion":[{"value":"2021-01-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2022-07-05","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}