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.
Press release: NWO Grants for Three UT Researchers