The paper “BDDs Strike Back: Efficient Analysis of Static and Dynamic Fault Trees” by Daniel Basgöze, Matthias Volk (Twente), Joost-Pieter Katoen, Shahid Khan and Marielle Stoelinga (Twente) as well as the paper “Configurable Benchmarks for C Model Checkers” by Xaver Fink, Philipp Berger and Joost-Pieter Katoen have been accepted for presentation at the NASA Formal […]

The paper entitled “Under-Approximating Expected Total Rewards in POMDPs” by Alexander Bork, Tim Quatmann and Joost-Pieter Katoen has been accepted for the 28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). The paper has also successfully passed all aspects of the artifact evaluation. The paper presents a novel algorithm […]

The paper entitled “ Model Checking Temporal Properties of Recursive Probabilistic Programs” by Tobias Winkler, Christina Gehnen and Joost-Pieter Katoen has been accepted at the 25th Int. Conf. on Foundations of Software Science and Computation Structure (FoSSaCS 2022). The paper presents decidability and complexity results for checking quantitative properties of visibly omega-regular languages against probabilistic […]

The paper entitled “Foundations for Entailment Checking in Quantitative Separation Logic” by Kevin Batz, Ira Fesefeldt, Marvin Jansen, Joost-Pieter Katoen, Florian Keßler, Christoph Matheja and Thomas Noll has been accepted for ESOP 2022, the 31st European Symposium on Programming. The paper presents the first results on decidability and complexity for entailment checking in quantitative separation […]

The paper entitled “Weighted Programming: A Programming Paradigm for Specifying Mathematical Models” by Kevin Batz, Adrian Gallus, Benjamin Kaminski, Joost-Pieter Katoen and Tobias Winkler has been accepted for OOPSLA 2022, which will be held as part of the ACM Conference on Systems, Programming, Languages, and Applications: Software for Humanity (SPLASH’22). The papers develops weakest-precondition- and weakest-liberal-precondition-style […]

The DFG has granted the RTG 2236 UnRAVeL (Uncertainty and Randomness in Algorithms, Verification and Logic) an extension to 2026. The research training group has been granted 12 PhD positions as well as 10 student-assistant position to continue our research. The second phase of UnRAVeL involves 12 PIs from CS, Mechanical Engineering, Business Economics, and […]

The paper “Convex Optimization for Parameter Synthesis in MDPs” by Murat Cubuktepe, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen and Ufuk Topcu has been accepted for publication in the journal IEEE Transactions on Automatic Control (impact factor 5,8). This paper formulates the feasibility problem for parametric MDPs (pMDPs) problem as a non-convex quadratically constrained quadratic program […]

The paper entitled “Synthesizing Optimal Bias in Randomized Self-Stabilization Algorithms” by Matthias Volk, Borzoo Bonakdarpour, Joost-Pieter Katoen and Saha Aflaki has been accepted for publication in the journal Distributed Computing. It presents a parameter-synthesis technique to automatically determine optimal biases of coin flips in randomised self-stabilisation algorithms.

Two papers of the MOVES group have been accepted at VMCAI 2022. The paper entitled “Out of Control: Reducing Probabilistic Models by Control-State Elimination” by Tobias Winkler, Johannes Lehmann and Joost-Pieter Katoen presents a static-analysis technique for reducing finite-state probabilistic models in the PRISM modeling language. The paper entitled “Gradient-Descent for Randomized Controllers under Partial […]

The paper entitled “Modelling and Analysis of Fire Sprinklers by Verifying Dynamic Fault Trees” by Shahid Khan, Joost-Pieter Katoen, Matthias Volk, Ahmad Zafar and Falak Sher has been accepted for presentation at the 10th Latin-American Symposium on Dependable Computing (LADC 2021). The paper models fire sprinkler systems in shopping centers by dynamic fault trees and […]