{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,23]],"date-time":"2026-04-23T06:00:01Z","timestamp":1776924001633,"version":"3.51.2"},"reference-count":43,"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:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"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>We focus on the integration of Formal Methods as mandatory theme in any Computer Science University curriculum. In particular, when considering the ACM Curriculum for Computer Science, the inclusion of Formal Methods as a mandatory Knowledge Area needs arguing for why and how does every computer science graduate benefit from such knowledge. We do not agree with the sentence \u201cWhile there is a belief that formal methods are important and they are growing in importance, we cannot state that every computer science graduate will need to use formal methods in their career.\u201d We argue that formal methods are and have to be an integral part of every computer science curriculum. Just as not all graduates will need to know how to work with databases either, it is still important for students to have a basic understanding of how data is stored and managed efficiently. The same way, students have to understand why and how formal methods work, what their formal background is, and how they are justified. No engineer should be ignorant of the foundations of their subject and the formal methods based on these.<\/jats:p>\n          <jats:p>In this article, we aim at highlighting why every computer scientist needs to be familiar with formal methods. We argue that education in formal methods plays a key role by shaping students' programming mindset, fostering an appreciation for underlying principles, and encouraging the practice of thoughtful program design and justification, rather than simply writing programs without reflection and deeper understanding. Since integrating formal methods into the computer science curriculum is not a straightforward process, we explore the additional question: what are the tradeoffs between one dedicated knowledge area of formal methods in a computer science curriculum versus having formal methods scattered across all knowledge areas? Solving problems while designing software and software-intensive systems demands an understanding of what is required, followed by a specification and formalizing a solution in a programming language. How to do this systematically and correctly on solid grounds is exactly supported by formal methods.<\/jats:p>","DOI":"10.1145\/3670795","type":"journal-article","created":{"date-parts":[[2024,6,10]],"date-time":"2024-06-10T11:11:52Z","timestamp":1718017912000},"page":"1-17","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":21,"title":["Does Every Computer Scientist Need to Know Formal Methods?"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2649-1752","authenticated-orcid":false,"given":"Manfred","family":"Broy","sequence":"first","affiliation":[{"name":"Informatik, Technische Universit\u00e4t M\u00fcnchen, Munchen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6355-1200","authenticated-orcid":false,"given":"Achim D.","family":"Brucker","sequence":"additional","affiliation":[{"name":"University of Exeter, Exeter, United Kingdom of Great Britain and Northern Ireland"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[{"name":"DINFO, University of Florence School of Engineering, Firenze, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9445-6863","authenticated-orcid":false,"given":"Mario","family":"Gleirscher","sequence":"additional","affiliation":[{"name":"University of Bremen, Bremen, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7079-0472","authenticated-orcid":false,"given":"Klaus","family":"Havelund","sequence":"additional","affiliation":[{"name":"Jet Propulsion Laboratory, California Inst. of Technology, Pasadena, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6972-2031","authenticated-orcid":false,"given":"Markus Alexander","family":"Kuppe","sequence":"additional","affiliation":[{"name":"Microsoft Research, Redmond, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8060-5920","authenticated-orcid":false,"given":"Alexandra","family":"Mendes","sequence":"additional","affiliation":[{"name":"INESC TEC, Faculty of Engineering, University of Porto, Porto, Portugal"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7238-5710","authenticated-orcid":false,"given":"Andr\u00e9","family":"Platzer","sequence":"additional","affiliation":[{"name":"Carnegie Mellon University, Pittsburgh, United States"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3610-3920","authenticated-orcid":false,"given":"Jan Oliver","family":"Ringert","sequence":"additional","affiliation":[{"name":"Bauhaus University Weimar, Weimar, Germany"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7400-2218","authenticated-orcid":false,"given":"Allison","family":"Sullivan","sequence":"additional","affiliation":[{"name":"The University of Texas at Arlington, Arlington, United States"}]}],"member":"320","published-online":{"date-parts":[[2024,12,26]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"Guide to the Software Engineering Body of Knowledge (SWEBOK\u00ae): Version 3.0 (3rd. ed.)","author":"Bourque Pierre","year":"2014","unstructured":"Pierre Bourque and Richard E. Fairley (Eds.). 2014. Guide to the Software Engineering Body of Knowledge (SWEBOK\u00ae): Version 3.0 (3rd. ed.). IEEE Computer Society Press, Washington, DC, USA."},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1109\/JPROC.2009.2037771"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_24"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.compenvurbsys.2019.101350"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-017-9426-4"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3338112"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/CVPR.2018.00175"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/3037697.3037739"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3520480"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/3586040"},{"key":"e_1_3_3_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-58298-2_1"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09836-5"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-023-01124-2"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3583083"},{"key":"e_1_3_3_18_2","volume-title":"Introduction to Computation and Programming using Python (Spring 2013 edition)","author":"Guttag John","year":"2013","unstructured":"John Guttag. 2013. Introduction to Computation and Programming using Python (Spring 2013 edition). MIT Press, Cambridge, Mass."},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/358549.358561"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_26"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/1232743.1232745"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2013.43"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2010.22"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.5555\/509043"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63588-0"},{"key":"e_1_3_3_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/3230977.3230981"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"},{"key":"e_1_3_3_30_2","unstructured":"EN50128: Railway applications - Communication signalling and processing systems Software for railway control and protection systems (2011)."},{"key":"e_1_3_3_31_2","volume-title":"Applying Viewpoints and Views to Software Architecture","author":"Rozanski Nick","year":"2005","unstructured":"Nick Rozanski and Eowin Woods. 2005. Applying Viewpoints and Views to Software Architecture. Open University White Paper."},{"key":"e_1_3_3_32_2","unstructured":"ISO26262: Road Vehicles - Functional Safety. International standard (2011)."},{"key":"e_1_3_3_33_2","unstructured":"ISO15408: Common Criteria for Information Technology Security Evaluation. International standard (2009)."},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1109\/52.976937"},{"key":"e_1_3_3_36_2","article-title":"Verifying executability of SysML behavior models using satisfiability modulo theory solvers","volume":"8283","author":"Barbau Raphael","year":"2020","unstructured":"Raphael Barbau and Conrad E. Bock. 2020. Verifying executability of SysML behavior models using satisfiability modulo theory solvers. NIST Technical Report 8283 (2020). Retrieved from https:\/\/nvlpubs.nist.gov\/nistpubs\/ir\/2020\/NIST.IR.8283.pdf","journal-title":"NIST Technical Report"},{"key":"e_1_3_3_37_2","doi-asserted-by":"publisher","DOI":"10.6028\/NIST.IR.8388"},{"key":"e_1_3_3_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-26236-4_16"},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1145\/2699417"},{"key":"e_1_3_3_40_2","article-title":"On formal methods thinking in computer science education","author":"Dongol Brijesh","year":"2023","unstructured":"Brijesh Dongol, Catherine Dubois, Stefan Hallerstede, Eric Hehner, Daniel Jackson, Carol Morgan, Peter M\u00fcller, Leila Ribeiro, A. Silva, Graeme Smith, and Eerke de Vink. 2023. On formal methods thinking in computer science education. Accepted by Form. Asp. Comput.","journal-title":"Accepted by Form. Asp. Comput"},{"key":"e_1_3_3_41_2","article-title":"Formal methods in industry","author":"Beek Maurice H. ter","year":"2023","unstructured":"Maurice H. ter Beek, Ron Chapman, Rance Cleaveland, Hubert Garavel, R. Gu, Ivo ter Horst, Jeroen J. A. Keiren, Thierry Lecomte, Michael Leuschel, Kristin Y. Rozier, Augusto Sampaio, Cristina Seceleanu, Martyn Thomas, Tim A. C. Willemse, and L. Zhang. 2023. Formal methods in industry. Submitted to Form. Asp. Comput.","journal-title":"Submitted to Form. Asp. Comput"},{"key":"e_1_3_3_42_2","article-title":"Should we teach formal methods or algorithmic problem solving, design patterns, model-driven engineering, software architecture, software product lines, requirements engineering, and security?","author":"Sekerinski Emil","year":"2023","unstructured":"Emil Sekerinski, Marsha Chechik, Joao F. Ferreira, John Hatcliff, Michael Hicks, and K. Lano. 2023. Should we teach formal methods or algorithmic problem solving, design patterns, model-driven engineering, software architecture, software product lines, requirements engineering, and security? In Preparation.","journal-title":"Preparation"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29510-7_5"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.5555\/1215128"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670795","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3670795","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:05:41Z","timestamp":1750291541000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3670795"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,12,26]]},"references-count":43,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2025,3,31]]}},"alternative-id":["10.1145\/3670795"],"URL":"https:\/\/doi.org\/10.1145\/3670795","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-01","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"}}]}}