Funded by: NWO (Open Competition)
Duration: January 2021 until December 2024
Researchers
Project summary
Who verifies the verifiers? Random hardware failures, random software crashes, random environmental effects, randomised algorithms: probabilistic effects are everywhere, and the critical systems we depend on—trains, air traffic control, electricity grids, communication infrastructure—must deal with them. Probabilistic verification software uses mathematical models to calculate the mean time to failure, expected energy consumption, or probability of recovery of such systems. Yet all software programmed by humans has bugs. In this project, we mathematically formalise probabilistic verification algorithms, use interactive theorem-proving systems to show their correctness, and automatically turn them into correct-by-construction software. Then, finally, probabilistic verification itself is verified.
Media
Press release: NWO Grants for Three UT Researchers