Tentative Author List:
- Maurice ter Beek
- Manfred Broy
- Brijesh Dongol
- Emil Sekerinski
Scope:
Formal Methods provide a wide range of techniques and tools for specifying, developing, analysing, and verifying software and hardware systems. In the papers, we make four key points: (1) Every Computer Science graduate needs to have an education in Formal Methods; (2) Formal Methods can support Teamwork, Code Review, Software Testing, and more; (3) Formal Methods are applicable in numerous domains (not only in safety-critical applications); and (4) The current offering of Formal Methods in the Computer Science education is inadequate.
Computer Science, namely the science of solving problems with software and software-intensive systems, provides the knowledge and skills to understand and capture precisely what a situation requires, and then develop a formal solution in a programming language. The most fundamental skill of a computer scientist, that of abstraction, is best addressed by Formal Methods. They provide the rigor for reasoning about goals, such as validation and verification, thus guaranteeing adequacy, accuracy, and correctness of implementations.
Formal Methods thinking, i.e., the ideas from Formal Methods applied in informal, lightweight, practical, and accessible ways, should be part of the recommended curriculum for every Computer Science student. Even students who train only in that “thinking” will become much better programmers. In addition, there are students who, exposed to those ideas, will be ideally positioned to study more: why the techniques work; how they can be automated; and how new ones can be developed. They could follow subsequently an optional path, including topics such as semantics, logics, and proof-automation techniques.
Formal Methods were conceived for teaching programming to novices more effectively than by informal reasoning and testing. Formal Methods explain algorithmic problem solving, design patterns, model-driven engineering, software architecture, software product lines, requirements engineering, and security. Formalisms can concisely and precisely express underlying fundamental design principles and equip programmers with a tool to handle related problems.
Formal Methods are becoming widely applied in industry, from eliciting requirements and early design to deployment, configuration, and runtime monitoring. Successfully applying Formal Methods in industry ranges from well-known stories in the safety-critical domain, such as railways and other transportation domains, to areas such as lithography manufacturing and cloud security in e-commerce, for example. Testimonies come from representatives who, either directly or indirectly, use or have used Formal Methods in their industrial project endeavours. Importantly, they are spread geographically, including Europe, Asia, North and South America.
ACM-CS2023 is the ideal time and place to adjust the way we teach Computer Science. There are mature tools and proofs of concept available and the possibility of designing coherent teaching paths. Importantly, this can be done without displacing the other “engineering” aspects of Computer Science already widely accepted as essential. Support for teachers is available.
Contact: Ana Cavalcanti, Luigia Petre
Current Version: