The paper “The Dial-a-Ride Problem in Primary Care with Flexible Scheduling” by Felix Engelhardt, Emma Ahrens, Christina Büsing together with Felix Rauh from University Leuven has been accepted for publication in the journal OR Spektrum. The paper generalizes the Dial-A-Ride problem, which models the transportation of patients in a rural area, such that it differentiates between chronic […]

The paper entitled “Foundations for Deductive Verification of Continuous Probabilistic Programs: From Lebesgue to Riemann and Back” by Kevin Batz, Joost-Pieter Katoen, Francesca Randone (University of Trieste), and Tobias Winkler has been accepted for the International Conference on Object-Oriented Programming Systems, Languages, and Application (OOPSLA 2025). The paper presents a new technique to formally check […]

The DFG together with the FNRS (Belgium) have granted the project, entitled “Mixing Formal Methods and Learning Techniques for Strategy Synthesis in Partially Observable Markov Decision Processes” for a period of three years. This project is a collaboration with the research group of Jean-Francois Raskin (Universite de Libre Bruxelles).

The paper “CERTPHASH: Towards Certified Perceptual Hashing via Robust Training” by Yuchen Yang (Johns Hopkins University), Qichang Liu (Tsinghua University), Christopher Brix, Huan Zhang (UIUC), and Yinzhi Cao (Johns Hopkins University) has been accepted for publication in the 34th USENIX Security Symposium. The paper proposes a novel technique to train neural networks to perform perceptual […]

The paper entitled “An Oracle-Guided Approach to Constrained Policy Synthesis Under Uncertainty” by Roman Andriushchenko, Milan Češka, Filip Macák (Brno University of Technology), Sebastian Junges (Radboud University) and Joost-Pieter Katoen has been accepted for publication in the Journal of Artificial Intelligence Research (JAIR). The paper present coloured Markov Decision Processes (MDPs) which describes a collection […]

The paper entitled “Fixed Point Certificates for Reachability and Expected Rewards in MDPs” by Tim Quatmann, Maximilian Schäffeler (TU Munich), Maximilian Weininger (ISTA), Tobias Winkler, Daniel Zilken and Krishnendu Chatterjee (ISTA) has been accepted at the 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2025), to be held […]

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