The proof is in the testing: The Swiss breakthrough that will make software more reliable
The size and complexity of today's software programs can make it difficult to check their likely reliability.
Testing only goes so far: often after applications are released, it's a wait-and-see strategy, with developers sending out patches for products if and when major problems become evident.
Two computer scientists at the Swiss Federal Institute of Technology (École Polytechnique Fédérale de Lausanne or EPFL) hope to change that - using automated reasoning tools to replace validating software through testing with more accurate formal mathematical proofs.
While verification tools have developed significantly over the years, one stumbling block has been support for proofs that use mathematical induction.
The EPFL research, by Viktor Kuncak, Associate Professor at the Laboratory for Automated Reasoning and Analysis and post-doctoral research fellow Andrew Reynolds, overcomes this by improving the inductive reasoning in Satisfiability Modulo Theories (SMT) solvers.
SMT solvers are next-generation verification programs for software and enhancing them with the ability to perform automated mathematical induction will enable them "to solve more problems in areas such as software and hardware verification," says Viktor Kuncak. This will in turn make software more reliable, improving the safety of systems we use everyday from air traffic control to health monitors.
The EPFL method relies on proving that if a theorem is true for one natural number it is for the one that follows (known as n+1). In particular, where it's not possible to verify an action directly, the technique breaks down tasks into smaller ones that it can resolve.
"The challenge often lies in discovery of intermediate lemmas, or subgoals, that are required for a proof to succeed. In the context of software verification, a subgoal may state a specific property of the output returned by a function call, or state that a property always holds during the execution of the program," said Reynolds.
Historically, discovering such subgoals relied on the developer. Now the new research shows that it can be done by automated reasoning tools.
Incorporating induction makes solvers - whether used with commercial verification tools like Coverity or open source academic tools like Leon, also developed at EPFL - more powerful and simpler to build.
The new technique is already publicly available inside CVC4 (Cooperating Validity Checker), an open-source SMT solver.
"For software verification applications, the tool is able to automatically prove the correctness of data structures, including binary search trees and sorted lists. In some cases, the tool is able to discover proofs that are simpler than ones that found by manual inspection from a user," said Reynolds.
"The hope is to enable mathematicians and computer scientists to focus on the most challenging portions of the mathematical proofs, while allowing an underlying automated reasoning tool to handle a majority of the steps in a proof.
"By increasing the amount of automation used in mathematical proofs, we likewise increase the size and complexity of theorems and systems that we are able to confidently reason about."
Read more on this story