The paper entitled “Bayesian Inference in Quantum Programs” by Christina Gehnen, Dominique Unruh and Joost-Pieter Katoen has been accepted for presentation at the 52nd EATCS International Colloquium on Automata, Languages, and Programming (ICALP 2025 – Track B). This paper considers postselection in quantum physics (aka: Bayesian conditioning in programs), for quantum while-programs, defines an operational […]

The papers “Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains” by Timm Spork, Christel Baier, Joost-Pieter Katoen, Sascha Klüppelholz, and Jakob Piribauer and “Efficient Probabilistic Model Checking for Relational Reachability” by Lina Gerlach, Tobias Winkler, Erika Ábrahám, Borzoo Bonakdarpour and Sebastian Junges have been accepted at the International Conference on Computer-Aided Verification (CAV) 2025. The first paper […]

The paper “Using GPUs And LLMs Can Be Satisfying for Nonlinear Real Arithmetic Problems” by Christopher Brix, Julia Walczak, Nils Lommen and Thomas Noll has been accepted for presentation at the VerifAI Workshop at ICLR 2025. The paper describes how satisfying assignments to quantifier-free NRA problems can be found using GPU acceleration, and how LLMs […]

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