Chalmers University of Technology
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 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.
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.
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.
/University Release. This material from the originating organization/author(s) might be of the point-in-time nature, and edited for clarity, style and length. Mirage.News does not take institutional positions or sides, and all views, positions, and conclusions expressed herein are solely those of the author(s).View in full here.
