Publications

2025
DOIRoman Andriushchenko, Alexander Nikolai Bork, Carlos E. Budde, Milan Češka, Kush Grover, Ernst Moritz Hahn, Arnd Hartmanns, Bryant Israelsen, Nils Jansen, Joshua Jeppson, Sebastian Junges, Maximilian A. Köhl, Bettina Könighofer, Jan Křetínský, Tobias Meggendorfer, David Parker, Stefan Pranger, Tim Quatmann, Enno Ruijters, Landon Taylor, Matthias Volk, Maximilian Weininger, Zhen Zhang. Tools at the Frontiers of Quantitative Verification : QComp 2023 Competition Report, TOOLympics challenge 2023 : updates, results, successes of the formal-methods competitions / dirk beyer, arnd hartmanns, fabrice kordon, editors, 90-146, Springer, 2025.
DOIRoman Andriushchenko, Milan Češka, Filip Macák, Sebastian Junges, Joost-Pieter Katoen. An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty, 433-469, AI Access Found., 2025.
DOIMarsha Chechik, Joost-Pieter Katoen. Introduction to the Special Collection from FM 2023, 1-2, Springer, 2025.
DOIHans Christian Hensel, Sebastian Junges, Tim Quatmann, Matthias Volk. Riding the Storm in a Probabilistic Model Checking Landscape, Principles of verification: cycling the probabilistic landscape : essays dedicated to joost-pieter katoen on the occasion of his 60th birthday : part II / nils jansen, sebastian junges, benjamin lucien kaminski, christoph matheja, thomas noll, tim quatmann, mariëlle stoelinga, matthias volk, editors, 98-114, Springer, 2025.
DOIKrishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Johannes Zilken. Fixed Point Certificates for Reachability and Expected Rewards in MDPs, 54 Seiten, 2025.
DOIDominik Geißler. Automata-based semantics for the probabilistic programming language ReDiP, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025.
DOIFelix Rauh, Emma Katharina Ahrens, Christina Maria Katharina Büsing, Martin Comis, Felix Engelhardt. The dial-a-ride problem in primary care with flexible scheduling, Springer, 2025.
DOITim Quatmann. What is the best algorithm for MDP model checking?, 431-437, Springer, 2025.
DOIKevin Batz, Joost-Pieter Katoen, Francesca Randone, Tobias Winkler. Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back, 95, ACM, 2025.
DOICarolina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour, Sebastian Junges. Efficient Probabilistic Model Checking for Relational Reachability (Extended Version), 30 Seiten, 2025.
DOIHossein Hojjat, Erika Ábrahám. Preface: Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023), 103244, Elsevier Science, 2025.
. Fundamentals of Software Engineering (extended versions of selected papers of FSEN 2023) : Special issue, Elsevier Science, 2025.
DOIMariia Anapolska, Emma Katharina Ahrens, Christina Maria Katharina Büsing, Felix Engelhardt, Timo Gersing, Corinna Marlene Mathwieser, Sabrina Schmitz, Sophia Wrede. Minimum‐Peak‐Cost Flows Over Time, 389-401, Wiley, 2025.
DOIKrishnendu Chatterjee, Tim Quatmann, Maximilian Schäffeler, Maximilian Weininger, Tobias Winkler, Daniel Johannes Zilken. Fixed Point Certificates for Reachability and Expected Rewards in MDPs; 1st ed. 2025, Tools and algorithms for the construction and analysis of systems : 31st international conference, TACAS 2025, held as part of the international joint conferences on theory and practice of software, ETAPS 2025, hamilton, on, canada, may 3–8, 2025, proceedings, part II / edited by arie gurfinkel, marijn heule, 130-151, Springer Nature Switzerland, 2025.
DOIEmil Beothy-Elo. Effective quantifier-based reasoning for quantitative deductive verification, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025.
DOIHannah Mertens, Joost-Pieter Katoen, Tim Quatmann, Tobias Winkler. Computing Expected Visiting Times and Stationary Distributions in Markov Chains: Fast and Accurate, 23, Springer Science + Business Media B.V., 2025.
DOICarolina Gerlach, Tobias Winkler, Erika Abraham, Borzoo Bonakdarpour, Sebastian Junges. Efficient Probabilistic Model Checking for Relational Reachability, Computer aided verification : 37th international conference, CAV 2025, zagreb, croatia, july 23-25, 2025, proceedings, part I, 127-147, Springer Nature Switzerland, 2025.
DOILutz Klinkenberg. Analysis of probabilistic programs using generating functions, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025.
DOIRaphael Jean Berthon, Joost-Pieter Katoen, Munyque Mittelmann, Aniello Murano. Robust Strategies for Stochastic Multi-Agent Systems, Proceedings of AAMAS-2025 / IFAAMAS, ACM (in cooperation) ; Y. Vorobeychik, S. Das, a. Nowé (eds.), 2437-2439, International Foundation for Autonomous Agents,Multiagent Systems (IFAAMAS), 2025.
Elbeck Lazaridi. Implementing the denotational semantics of probabilistic programs, 2025.
DOIAlexander Nikolai Bork, Tim Quatmann, Joost-Pieter Katoen, Svenja Maria Stein. Multi-Cost-Bounded Reachability Analysis of POMDPs, Conference on uncertainty in artificial intelligence, 21-25 july 2025, rio othon palace, rio de janeiro, brazil / editors: Silvia chiappa, sara magliacane, 354-366, 2025.
DOIKaleb Kierner. Modeling non-deterministic quantum programs for model checking, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025.
DOIMarcel Eissing. On the relation of rely-guarantee and assume-guarantee reasoning, 1 Online-Ressource : Illustrationen, RWTH Aachen University, 2025.
DOITimm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, Jakob Piribauer. Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains, Computer aided verification : 37th international conference, CAV 2025, zagreb, croatia, july 23-25, 2025, proceedings, part II, 56-81, Springer Nature Switzerland, 2025.
Johannes Peter Valentin Gaidetzka. Quantum circuit optimization through eliminating and deferring mid-circuit measurements, 2025.