The paper entitled “Quantifier Elimination and Craig Interpolation: The Quantitative Way” byKevin Batz, Joost-Pieter Katoen and Nora Orhan has been accepted at the FoSSaCS 2025 Conference (Hamilton, Canada). This paper gives a quantifier elimination algorithm for quantitative formulas as they e.g. occur in the analysis of probabilistic programs, and present a theorem for a quantitative […]

The paper entitled “Robust Strategies for Stochastic Multi-Agent Systems” by Raphael Berthon, Joost-Pieter Katoen, Munyque Mittelmann, and Aniello Murano has been accepted as extended abstract at the 24th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2025), Detroit. The paper presents Probabilistic Alternating-Time Temporal Logic with bounded strategies (PATLb) for stochastic multi-agent systems with uncertainty, and […]

The paper “Scalable Neural Network Verification with Branch-and-bound Inferred Cutting Planes” by Duo Zhou (University of Illinois Urbana-Champaign), Christopher Brix, Grani A Hanasusanto (Illinois) and Huan Zhang (Illinois) has been accepted for the Thirty-Eighth Annual Conference on Neural Information Processing Systems (NeurIPS 2024) in Vancouver. The paper describes how the branch-and-bound process in neural network […]

On the occasion of Joost-Pieter Katoen’s 60th birthday, a Colloquium on Principles of Verification was organised on November 7, 2024. It attracted more than 100 participants from all over the world and was opened by welcoming speeches by representatives of both the University of Twente (NL) and RWTH Aachen University. Moreover, it featured eleven scientific […]

The paper “A Taxonomy of Hoare-Like Logics: Towards a Holistic View using Predicate Transformers and Kleene Algebras with Top and Tests” by Lena Verscht and Benjamin Kaminski has been accepted for the 52nd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2025) in Denver. The paper provides an overview of program logics, including Hoare […]

The paper “Markov Decision Processes with Sure Parity and Multiple Reachability Objectives” by Raphaël Berthon, Joost-Pieter Katoen and Tobias Winkler has been accepted for the 18th Int. Conference on Reachability Problems (RP 2024) in Vienna. The paper presents new algorithms and complexity bounfs to achieve one sure parity condition and several quantitative threshold objectives on […]

The paper entitled “A Spectrum of Approximate Probabilistic Bisimulations” by Timm Spork (TU Dresden), Christel Baier (TU Dresden), Joost-Pieter Katoen, Jakob Piribauer (TU Dresden) and Tim Quatmann has been accepted for the 35th Int. Conf. on Concurrency Theory (CONCUR) in Calgary, Canada. The paper compares several different (and some new) notions of approximate strong and […]

The paper entitled “Accurately Computing Expected Visiting Times and Stationary Distributions in Markov Chains” by Hannah Mertens, Joost-Pieter Katoen, Tim Quatmann and Tobias Winkler has received the EAPLS (Eur. Association of Programming Languages) Best Paper Award@ETAPS 2024. The paper provides efficient and scalable algorithms to compute expected visiting times in Markov chains, and shows how […]

Joost-Pieter Katoen has been elected as member of Leopoldina, the German Academy of Sciences. This academy was established in 1652 and is the oldest academy in the world. Katoen is the first computer scienttist from RWTH Aachen University in Leopoldina and the 15th RWTH member of Leopoldina ever. See also press announcements: https://www.rwth-aachen.de/cms/root/Die-RWTH/Aktuell/Pressemitteilungen/Maerz-2024/~bgppks/Joost-Pieter-Katoen-in-die-Leopoldina-au/lidx/1/ and https://www.utwente.nl/en/eemcs/news/2024/3/1415316/professor-joost-pieter-katoen-inducted-into-the-leopoldina-academy-of-sciences

The paper entitled “Exact Bayesian Inference for Loopy Probabilistic Programs Using Generating Functions” by Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase and Joost-Pieter Katoen has been accepted for the Conference Object-Oriented Programming, Systems, Languages, and Applications 2024 (OOPSLA). The paper presents a novel exact inference technique for discrete probabilistic programs with unbounded loops and conditioning. […]