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. As a
Wallenberg Academy Fellow, Niki Vazou wants to develop a method that is
both easy to use, and rests on 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
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.
Reliable and maintainable systems
In her research, Niki Vazou, currently working at the IMDEA Software Institute in Spain, aims to make concepts of program verification mainstream and integrate them with functional programming. This will lead to the development of more reliable and maintainable programs that are also easier to develop.
"The impact will appear in all areas of society that rely on software, ranging from social networking, to monetary transactions and development of safe medical equipments" says Niki Vazou.
The propsed new method for formal verification that can both be integrated in the software and simultaneously generate a mathematical proof of a correct test.
If Niki Vazou accepts the appointment to Wallenberg Academy Fellow she will conduct her research at the Department of Computer Science and Engineering.
"My interest in functional programming comes from a huge love of mathematics, and the discovery that mathematical functions can become interactive through programming languages such as Prolog and Haskell. Chalmers is the best European university in the fields of functional programming and type theory, and since my research is exactly at the intersection of these two areas, the appointment to the Wallenberg Academy Fellow provides a unique opportunity to collaborate directly with top researchers in my field", says Niki Vazou.
Four Wallenberg Academy Fellows to Chalmers 2021
The research funding from the Wallenberg Academy Fellowship is SEK 7.5 million over 5 years, with the possibility of extension. Here you can read about the other appointments.