Moves News

Two papers at NFM 2022

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

Paper at TACAS 2022

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

Paper at FoSSaCS 2022

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

Paper at ESOP 2022

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

Paper at OOPSLA 2022

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

RTG UnRAVeL Extended

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

Paper in IEEE TAC

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

Paper in Distributed Computing

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 at VMCAI 2022

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

Paper at SEFM 2021

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