Correctness through formal methods

Formal methods are crucial for ensuring software correctness. They enable mathematical proofs of freedom from errors in safety-critical systems. The use of proof assistants and automated tools significantly increases the quality of software. These methods complement conventional tests and provide valuable insights into the reliability of software.

Podcast on formal methods

In the latest episode of the Software Testing Podcast, we celebrate World Quality Week. I talk to Lars and Bianca about how to mathematically prove freedom from defects in software and which tools can help. Bianca uses examples from the financial and automotive industries to explain why certain systems require absolute freedom from errors. Lars complements the conversation with insights into formal methods and how they are applied in practice. One particularly interesting topic was how AI can support us in providing evidence.

“I can’t prove freedom from errors with tests. There are simply certain domains where I need to be able to prove the absence of errors.” - Lars Hupel, Bianca Lutz

Lars Hupel is Chief Evangelist for Digital Currencies at Giesecke+Devrient, an international security technology company. As part of this role, Lars holds and writes numerous lectures, workshops and articles to make the technology behind digital currencies accessible to a broad audience. With a background as a software developer, Lars also contributes to product development and represents the company on various industry bodies. Lars holds a PhD in logic and verification from the Technical University of Munich and uses this knowledge to make Giesecke+Devrient’s products even more secure.

Bianca Lutz is a software architect at Active Group GmbH and works from Berlin. She was already interested in formal methods during her studies and worked with the proof assistant Isabelle/HOL. However, she is still fascinated by technical topics such as operating systems, especially embedded systems. She has been involved in various scientific publications, is a Linux kernel contributor and has published in Isabelle’s Archive of Formal Proofs as part of her thesis. After working in the insurance industry for several years, where she mainly dealt with legacy code, she switched to the functional programming camp in 2022.

Highlights of the Episode

• In areas such as finance and medicine, accuracy is crucial, and formal methods can help.
• Formal methods use mathematical models and proof assistants to avoid software errors.
• Microsoft uses automated tools to check drivers for errors.
• Formal methods are not a panacea, but complement other testing methods.
• Changes in the software can lead to complex adjustments in the proofs.

Software quality and formal methods

Why flawlessness is important

In the field of software testing, absolute freedom from errors is difficult to guarantee. However, in certain industries - such as finance, automotive or medical technology - the requirements for freedom from errors are particularly high, as even small errors can have drastic consequences. For this reason, systems in such areas must be tested and validated with particular care.

The role of formal methods

Tests alone are often not enough to ensure complete correctness in safety-critical systems. Formal methods are used here and make it possible to provide mathematically rigorous proofs of the correctness of software. The use of proof assistants ensures that there are no logical gaps in the reasoning and checks. These methods complement conventional tests and increase the reliability of the results.

Practical applications and challenges

In practice, formal methods are often associated with considerable additional work. For example, it may be necessary to write up to ten lines of proof code for each line of regular code. Nevertheless, there are also less complex approaches such as type systems or model checkers, which are less comprehensive but still provide valuable insights and increase the quality of testing.

Automation and AI support

Automation and artificial intelligence (AI) are playing an increasingly important role in the creation of formal proofs. Some modern tools, such as Isabel, already use machine learning algorithms to generate proofs faster and significantly reduce manual effort. Such automated processes make the application of formal methods more efficient and accessible.

Conclusion and outlook

The combination of tests and formal methods is crucial to ensure the highest software quality. These techniques are not a stand-alone solution, but a valuable addition to traditional testing methods. Advances in the field of AI open up new opportunities to further develop these methods and make them even more widely applicable. The future therefore promises exciting developments in the interaction between AI and formal verification.

Frequently asked questions about formal methods