Formal Methods
Software systems control ever more aspects of our lives, making the security and safety of these systems increasingly relevant, in two senses: Safety when it concerns life, limb, or business-critical areas, and security against intrusions, sabotage, and data leaks. For such software, we want the software to guarantee that it meets certain requirements. Simple tests are not sufficient for this, as they typically only cover specific scenarios – we want the software to behave correctly in all scenarios. This requires the application of mathematical techniques – so-called formal methods, which until now were a gap in the portfolio of Advanced trainings that we have now closed.
The module "FM – Formal Methods" teaches software architects how they can ensure the correctness of a system's design and implementation through mathematical proofs. The module focuses on safety-critical, sensitive, or economically vital systems and goes beyond traditional architecture and testing methods by providing formal techniques to verify that software meets its requirements. By integrating formal methods early in the design phase, architects can create verifiable models that ensure a higher degree of software quality and reliability.
Special prior knowledge in mathematics or these technologies is not required. A previously attended iSAQB Advanced training on Functional Software Architecture or Domain-Specific Languages is not a mandatory prerequisite but facilitates understanding.
iSAQB Advanced Level
This training is part of the Advanced Level of the iSAQB certification for software architects (CPSA-A) and implements the iSAQB module FM.
If you attend this training as part of the iSAQB Advanced Level, you can have credit points recognized afterwards (10 credit points in the Methodology competence area and 20 credit points in the Technical Competence area).
Content
- Mathematical foundations
- Specification and implementation
- Development processes with formal methods
- Concrete techniques and tools: proof assistants, model checking, SMT solvers
Upcoming Dates
2026-11-30 – 2026-12-02, online
Instructor(s)
Dr. Michael Sperber
Dr. Sperber is the managing director of Active Group GmbH, which develops custom software exclusively using functional programming. He is an expert in functional programming and has been applying it for over 25 years in research and industrial development. Dr. Sperber has also been involved in programming education for over 30 years and has conducted extensive research on the topic. He is co-founder of the blog funktionale-programmierung.de and co-organizer of the developer conference BOB, as well as author of several books and numerous technical articles.
Bianca Lutz
Bianca Lutz is a software architect at Active Group GmbH and works from Berlin. She has many years of experience in application development, the application of formal methods in software engineering, and is a certified expert in requirements engineering.
Christina Zeller
Christina Zeller studied pedagogy, psychology, and computer science, and has researched and taught in a university setting on machine learning, cognitive science, and robotics. She gained extensive experience in software architecture and functional programming at a start-up and is currently expanding this knowledge as a software architect at Active Group GmbH.
Markus Schlegel
Markus Schlegel is a software architect at Active Group GmbH. Markus discovered functional programming in 2013 and has slept peacefully ever since.