{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,18]],"date-time":"2026-03-18T09:51:13Z","timestamp":1773827473615,"version":"3.50.1"},"reference-count":41,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2024,12,26]],"date-time":"2024-12-26T00:00:00Z","timestamp":1735171200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,3,31]]},"abstract":"<jats:p>Formal Methods (FMs) radically improve the quality of the code artefacts they help to produce. They are simple, probably accessible to first-year undergraduate students and certainly to second-year students and beyond. Nevertheless, in many cases, they are not part of a general recommendation for course curricula, i.e., they are not taught \u2014 and yet they are valuable.<\/jats:p>\n          <jats:p>\n            One reason for this is that teaching \u201cFormal Methods\u201d is often confused with teaching logic and theory. This article advocates what we call\n            <jats:italic>FM thinking<\/jats:italic>\n            : the application of ideas from\n            <jats:italic>Formal<\/jats:italic>\n            Methods applied in informal, lightweight, practical and accessible ways. We will argue here that\n            <jats:italic>FM thinking<\/jats:italic>\n            should be part of the recommended curriculum for every Computer Science student, for even students who train only in that \u201cthinking\u201d will become much better programmers. However, there will be others who, exposed to those ideas, will be ideally positioned to go further into the more theoretical background: why the techniques work, how they can be automated, and how new ones can be developed. Those students would follow subsequently a specialised, more theoretical stream, including topics such as semantics, logics, verification and proof-automation techniques.\n          <\/jats:p>","DOI":"10.1145\/3670419","type":"journal-article","created":{"date-parts":[[2024,6,1]],"date-time":"2024-06-01T09:07:34Z","timestamp":1717232854000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":14,"title":["On Formal Methods Thinking in Computer Science Education"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0446-3507","authenticated-orcid":false,"given":"Brijesh","family":"Dongol","sequence":"first","affiliation":[{"name":"University of Surrey, Guildford, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9477-8109","authenticated-orcid":false,"given":"Catherine","family":"Dubois","sequence":"additional","affiliation":[{"name":"Ecole Nationale Sup\u00e9rieure d'Informatique pour l'Industrie et l'Enterprise, Evry, France"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9952-0214","authenticated-orcid":false,"given":"Stefan","family":"Hallerstede","sequence":"additional","affiliation":[{"name":"Aarhus Universitet, Aarhus, Denmark"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0179-0097","authenticated-orcid":false,"given":"Eric","family":"Hehner","sequence":"additional","affiliation":[{"name":"University of Toronto, Toronto, Canada"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8535-9068","authenticated-orcid":false,"given":"Carroll","family":"Morgan","sequence":"additional","affiliation":[{"name":"University of New South Wales, Sydney, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7001-2566","authenticated-orcid":false,"given":"Peter","family":"M\u00fcller","sequence":"additional","affiliation":[{"name":"ETH Zurich, Zurich, Switzerland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7039-092X","authenticated-orcid":false,"given":"Leila","family":"Ribeiro","sequence":"additional","affiliation":[{"name":"Federal University of Rio Grande do Sul, Porto Alegre, Brazil"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5014-9784","authenticated-orcid":false,"given":"Alexandra","family":"Silva","sequence":"additional","affiliation":[{"name":"Cornell University, Ithaca, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1019-4761","authenticated-orcid":false,"given":"Graeme","family":"Smith","sequence":"additional","affiliation":[{"name":"School of EECS, The University of Queensland, Brisbane, Australia"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9514-2260","authenticated-orcid":false,"given":"Erik","family":"de Vink","sequence":"additional","affiliation":[{"name":"Eindhoven University of Technology, Eindhoven, Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2024,12,26]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91550-6_1"},{"key":"e_1_3_3_3_1","volume-title":"CS2023: ACM\/IEEE-CS\/AAAI Computer Science Curricula","author":"ACM Association for Computing Machinery","year":"2023","unstructured":"Association for Computing Machinery ACM. 2023. CS2023: ACM\/IEEE-CS\/AAAI Computer Science Curricula. ACM. https:\/\/csed.acm.org\/"},{"key":"e_1_3_3_4_1","volume-title":"A Taxonomy for Learning, Teaching, and Assessing: A Revision of Bloom\u2019s Taxonomy of Educational Objectives","author":"Anderson Lorin","year":"2001","unstructured":"Lorin Anderson, David Krathwohl, Peter Airasian, Kathleen Cruikshank, Richard Mayer, Paul Pintrich, James Raths, and Merlin Wittrock. 2001. A Taxonomy for Learning, Teaching, and Assessing: A Revision of Bloom\u2019s Taxonomy of Educational Objectives. Pearson."},{"key":"e_1_3_3_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/S00165-008-0070-Y"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.4230\/DagRep.5.2.44"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32441-4_4"},{"key":"e_1_3_3_8_1","volume-title":"Taxonomy of Educational Objectives: The Classification of Educational Goals. Vol. Handbook I: Cognitive Domain.","author":"Bloom B. S.","year":"1956","unstructured":"B. S. Bloom, M. D. Engelhart, E. J. Furst, W. H. Hill, and D. R. Krathwohl. 1956. Taxonomy of Educational Objectives: The Classification of Educational Goals. Vol. Handbook I: Cognitive Domain.David McKay Company."},{"key":"e_1_3_3_9_1","volume-title":"SWEBOK: Guide to the Software Engineering Body of Knowledge (Version 3.0)","author":"Bourque Pierre","year":"2004","unstructured":"Pierre Bourque and Richard E. Fairley (Eds.). 2004. SWEBOK: Guide to the Software Engineering Body of Knowledge (Version 3.0). IEEE Comp. Soc."},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27534-0_2"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3670795"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-20398-5_33"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96142-2_26"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/1614191"},{"key":"e_1_3_3_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-32441-4"},{"key":"e_1_3_3_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27534-0"},{"key":"e_1_3_3_17_1","volume-title":"How to Design Programs: An Introduction to Programming and Computing","author":"Felleisen Matthias","year":"2018","unstructured":"Matthias Felleisen, Robert Bruce Findler, Matthew Flatt, and Shriram Krishnamurthi. 2018. How to Design Programs: An Introduction to Programming and Computing. MIT Press."},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-91550-6"},{"key":"e_1_3_3_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_3_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000113"},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3357231"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/52.896248"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-57663-9_12"},{"key":"e_1_3_3_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4419-8596-5"},{"key":"e_1_3_3_25_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. MIT Press. 609\u2013619 pages."},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/3338843"},{"issue":"4","key":"e_1_3_3_27_1","first-page":"21","article-title":"Lightweight formal methods","volume":"29","author":"Jackson Daniel","year":"1996","unstructured":"Daniel Jackson and Jeannette Wing. 1996. Lightweight formal methods. IEEE Comput. 29, 4 (1996), 21\u201322.","journal-title":"IEEE Comput."},{"key":"e_1_3_3_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3605215"},{"key":"e_1_3_3_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"e_1_3_3_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_3_31_1","volume-title":"Program Proofs","author":"Leino K. Rustan M.","year":"2023","unstructured":"K. Rustan M. Leino. 2023. Program Proofs. MIT Press."},{"key":"e_1_3_3_32_1","volume-title":"Program Development in Java - Abstraction, Specification, and Object-Oriented Design","author":"Liskov Barbara","year":"2001","unstructured":"Barbara Liskov and John V. Guttag. 2001. Program Development in Java - Abstraction, Specification, and Object-Oriented Design. Addison-Wesley."},{"key":"e_1_3_3_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/197320.197383"},{"key":"e_1_3_3_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/534929"},{"key":"e_1_3_3_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29628-9_1"},{"key":"e_1_3_3_36_1","volume-title":"An Introduction to Programming and Object-oriented Design Using Java","author":"Ni\u00f1o Jaime","year":"2008","unstructured":"Jaime Ni\u00f1o and Frederick A. Hosch. 2008. An Introduction to Programming and Object-oriented Design Using Java. John Wiley & Sons, Inc."},{"key":"e_1_3_3_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17601-3_1"},{"key":"e_1_3_3_38_1","unstructured":"Benjamin Pierce Arthur Azevedo de Amorim Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2010. Software foundations. (2010). Retrieved from https:\/\/softwarefoundations.cis.upenn.edu\/"},{"key":"e_1_3_3_39_1","volume-title":"The Cyber Security Body of Knowledge","author":"Rashid Awais","year":"2021","unstructured":"Awais Rashid, Howard Chivers, Emil Lupu, Andrew Martin, and Steve Schneider (Eds.). 2021. The Cyber Security Body of Knowledge. University of Bristol. https:\/\/www.cybok.org"},{"key":"e_1_3_3_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-89159-6_17"},{"key":"e_1_3_3_41_1","volume-title":"Concepts, Techniques, and Models of Computer Programming","author":"Roy Peter Van","year":"2004","unstructured":"Peter Van Roy and Seif Haridi. 2004. Concepts, Techniques, and Models of Computer Programming. MIT Press. http:\/\/www.info.ucl.ac.be\/people\/PVR\/book.html"},{"key":"e_1_3_3_42_1","article-title":"Formal methods in industry","author":"Beek M. ter","year":"2024","unstructured":"M. ter Beek, R. Chapman, R. Cleaveland, H. Garavel, R. Gu, I. ter Horst, J. Keiren, T. Lecomte, M. Leuschel, K. Rozier, A. Sampaio, C. Seceleanu, M. Thomas, T. Willemse, and L. Zhang. 2024. Formal methods in industry. Formal Aspects Comput. (2024). IN THIS ISSUE.","journal-title":"Formal Aspects Comput."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670419","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3670419","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:38Z","timestamp":1750291538000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670419"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,26]]},"references-count":41,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3670419"],"URL":"https:\/\/doi.org\/10.1145\/3670419","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"value":"0934-5043","type":"print"},{"value":"1433-299X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,12,26]]},"assertion":[{"value":"2023-07-24","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-05-20","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-12-26","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}