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 tool paper entitled “A Debugger for Probabilistic Programs” by Alexander Hoppen and Thomas Noll has been accepted for presentation at the 19th International Conference on Software Engineering and Formal Methods (SEFM 2021). The paper presents both a theoretical foundation and a prototype implementation of a recording-based debugger for imperative probabilistic programs supporting randomised choice, […]

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 […]

The paper entitled “DFT Modeling Approach for Operational Risk Assessment of RailwayInfrastructure” by Matthias Volk, Norman Weik (DLR), Nils Nießen, and Joost-Pieter Katoen has been accepted for publication in the journal Software Tools for Technology Transfer (STTT). The paper is an extension of the FMICS 2019 paper (awarded the best paper award) and presents a […]