NWO VENI Grants for Thomas Neele and Matthias Volk

19-Sep-2024

The NWO VENI grant is a personal scientific grant as part of the NWO Talent Programme and is aimed at excellent researchers at the start of their career. This year, two VERSEN members from Eindhoven University of Technology are among the awarded researchers: Thomas Neele and Matthias Volk. Both awardees are part of the Formal System Analysis group at TU/e and their research aims to improve system reliability through mathematical rigorous techniques.

Thomas Neele: Explainable formal methods with certificates

While formal analysis techniques for software can reduce the surging risks associated with it, we lack analysis methods that can produce correctness certificates of industrial-size software. The need for such a method has recently become evident after the discovery of errors in several established analysis techniques. In this project, Thomas Neele will integrate scalable analysis and the creation of compact certificates. Independent (automated) verification of those certificates offers nigh absolute certainty about the analysis result. This will raise standard for verification of safety-critical software far beyond the current practice.

Neele: “With this grant, I will be able to increase the scalability of certification through model checking and thus improve its applicability to large systems. I hope that this approach will become wide-spread in development of future systems.”

Matthias Volk: UNcertaInty In COntinuous-time maRkov chaiNs (UNICORN)

Ensuring the safety and reliability of complex, high-tech systems is of utmost importance. Formal methods allow for the checking of requirements such as ‘the probability of a system failure within a year is below a certain threshold’. However, applying these techniques requires precise knowledge of the probabilities of component failures. In this project, Matthias Volk seeks to develop analysis techniques for systems with unknown or imprecise probabilities. The new techniques allow to ensure that the overall safety requirements are met, even if there is uncertainty in the component failures.

Volk: “A special focus of this project is to provide ready-to-use tool support for practical applications, for example sensitivity analysis in reliability models or optimal maintenance planning under uncertainty.”