NWO VIDI Grant for Arnd Hartmanns


The NWO VIDI grant supports researchers in the phase of establishing a research group or expanding their recent research group. This year, one VERSEN member is among the awarded researchers: Arnd Hartmanns (University of Twente, Enschede). His research is in the area of formal methods, aiming at improving the reliability of systems and software through mathematically rigorous techniques.

Arnd Hartmanns: Trustworthy Analysis of Stochastic Timed Systems 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. Domain experts use design and verification tools to create these systems and ensure they are reliable. But how to ensure this software is correct? In this project, Arnd Hartmanns will work towards combining mathematics and computer science to develop verification software that cannot be wrong: Because its algorithms have been machine-checked with an interactive theorem prover; and the theorem prover equally shows that the software itself implements these algorithms correctly through a series of refinement proofs down to LLVM bytecode.