Funded by: NWO (VIDI)
Duration: July 2024 until June 2029
Researchers
Project summary
We rely on storm surge barriers, nuclear power plants, and other critical systems to work safely even when operators make errors or equipment fails at inconvenient random moments. Experts use special software to design these systems and ensure they are reliable. But how to ensure this software is correct? This research combines mathematics and computer science to develop software for the experts that cannot be wrong: Its algorithms come with mathematical proofs of correctness that have been checked by a computer using a so-called theorem prover; and the theorem prover equally shows that the software itself implements these algorithms correctly.
Media
Press release: VIDI Funding for Four UT Research Projects