The Association for Computing Machinery (ACM, https://www.acm.org/) has been publishing guidelines for Computer Science (CS) university curricula for more than five decades. Since the field of CS evolves quickly, ACM revises its guidelines once every decade. The latest revision, CS2023, recently published, contains 17 core knowledge areas deemed essential for CS, each of which further divided into knowledge units made of topics, some mandatory to teach and some elective.
The Role of Formal Methods in Computer Science Education is pointed out in a recent article which summarises discussion and evidence brought forward in three white papers--altogether authored by 35 computer scientists and practitioners worldwide with extensive experience in teaching Formal Methods in Academia or working with them in Industry. This key role of Formal Methods must thus be reflected in CS curricula as a core knowledge area rather than as elective topics in distinct knowledge areas. This is confirmed by an extensive review of the increasing use of Formal Methods in Industry--not limited to the well-known success stories from the safety-critical domain, but including use cases in lithography manufacturing and cloud security in e-commerce as well as industrial use in Europe, Asia, and North and South America. Both the article and the review were coordinated by the head of the Formal Methods and Tools (FMT) laboratory of the CNR Institute of Information Science and Technologies "A. Faedo" (ISTI), and they have been published in leading CS journals from ACM. Formal Methods are languages and techniques (and tools) based on rigorous mathematical foundations for the specification, development, and (manual or automated) analysis and verification of software and hardware systems. FMT is an internationally renowned research group in the field, with decades of experience in the development and application of Formal Methods and tools, in particular in the Railway Industry.
The article thus argues for the need to introduce Formal Methods as a distinct core knowledge area in the ACM/IEEE/AAAI CS curricula guidelines (https://csed.acm.org/), since currently Formal Methods are covered only as elective topics in some knowledge units of the knowledge areas Foundations of Programming Languages and Software Engineering. The evidence put forward suggests that the lack of indicating Formal Methods as a core knowledge area in the CS2023 guidelines is unjustified, arguably similar to the fact that just 10 years ago Artificial Intelligence was not included in the CS2013 guidelines. In particular, the importance of Formal Methods thinking in CS education is put forward, since this provides the necessary rigour in reasoning about software, its specification, its verification, and its correctness--all fundamental skills for future software developers. Then, the importance of knowing Formal Methods is put forward--for all computer scientists, since the skills and knowledge acquired in this way provide the indispensable solid foundation that forms the backbone of CS practice. Finally, it is underlined that teaching Formal Methods need not come at the cost of displacing other engineering aspects of CS that are already widely accepted as essential. On the contrary, it is shown that Formal Methods have the potential to support and strengthen the presentation and knowledge in eight of the 17 knowledge areas of CS2023; next to the abovementioned knowledge areas, these are Algorithmic Foundations, Architecture and Organization, Artificial Intelligence, Parallel and Distributed Computing, Security, and Software Development Fundamentals. The article provides concrete suggestions for educators on how to incorporate Formal Methods into CS education, for example via Formal Methods Europe (FME, https://fmeurope.org/) and its Teaching Committee's Education Course Database (https://fme-teaching.github.io/courses/).
References:
M. ter Beek, M. Broy, and B. Dongol, The Role of Formal Methods in Computer Science Education. ACM Inroads 15, 4 (2024), 58-66. DOI: https://doi.org/10.1145/3702231
M.H. ter Beek, R. Chapman, R. Cleaveland, H. Garavel, R. Gu, I. ter Horst, J.J.A. Keiren, T. Lecomte, M. Leuschel, K.Y. Rozier, A. Sampaio, C. Seceleanu, M. Thomas, T.A.C. Willemse, and L. Zhang, Formal Methods in Industry. Formal Aspects of Computing: Applicable Formal Methods (2024). DOI: https://doi.org/10.1145/3689374
Focus