New method for software verification

Developers can currently choose between two methods for verifying that software works correctly: one is impractical to use, but rigorous; the other is easier to use, but less reliable. Wallenberg Academy Fellow Niki Vazou will now develop a method that is both practicable and has a rigorous foundation. 

The software used for bank transactions, smart vehicles or health care equipment, for example, must function correctly when it is implemented. To ensure this, developers use something called formal verification, which could involve testing that no confidential information leaks from the system, or that encryption functions as it should. 

There are currently two methods for formal verification. The traditional form uses a branch of mathematics called type theory; if the code works, the verification will generate a mathematical proof of correctness. This method is therefore rigorous but, for various reasons, impractical to use. 

Instead, many developers work with another method, type systems for refinements, which can be developed in common programming languages. This is a practical form of verification and can be integrated in the software. However, this system does not rest on the same strong mathematical foundation.

Dr Niki Vazou at IMDEA Software Institute, Spain, will now develop a method for formal verification that can both be integrated in the software and simultaneously generate a mathematical proof of a correct test.

As a Wallenberg Academy Fellow, she will work at Chalmers University of Technology. 

Photo: Niki Vazou