NWO VENI Grants for two VERSEN members

01-Sep-2023

The NWO VENI grant targets excellent researchers who have recently obtained their PhDs. This year, two VERSEN members are among the awarded researchers: Clemens Dubslaff (Eindhoven University of Technology) and Sebastian Junges (Radboud University, Nijmegen). Both awardees are conducting research in the area of formal methods, aiming at improving software reliability through mathematical rigorous techniques.

Clemens Dubslaff: Quasi Decision Diagrams for Symbolic Verification and Explainability

Formal verification methods such as symbolic model checking are a cornerstone for improving reliability of computing systems. However, existing methods do not scale well and can barely provide explanations of the verification results due to their exhaustive exploration approach. In his Veni-funded project, Clemens Dubslaff will tackle both limitations, developing a new data structure of quasi decision diagrams to model lazy decision making. With such decision diagrams, an exhaustive analysis can be avoided by lazily refining relevant decisions only. This potentially unlocks new limits on scalability of symbolic model checking and provides new opportunities for explanation, e.g., through causal reasoning on relevant refinements.

Dubslaff: “This Veni grant gives me the opportunity to shape a challenging research line that connects new verification theory and practical explanations towards reliable and understandable computing systems of the future.”

Sebastian Junges: Symbolic Probabilistic Model Checking with Massive Design Spaces

The design of safety-critical systems comes with many questions: What is the most cost-efficient hardware for lane assist in cars? What battery size suffices for a satellite? Will the robot safely unload the dishwasher? Although seemingly different, these questions can all be (partially) answered by analyzing Markov models that describe how systems behave in uncertain circumstances. However, the complexity of modern computer systems leads to models that are too big to handle. In this research project, Sebastian Junges aims to develop novel algorithms that are able to analyse much bigger Markov models.

Junges: “With this project, we make it easier for researchers and practitioners to analyze huge Markov models. A particular focus of this project is to support use-cases in which a set of competing designs are analyzed.”