The paper entitled “Finding an ϵ-Close Minimal Variation of Parameters in Bayesian Networks” by Bahare Salmani and Joost-Pieter Katoen has been accepted for presentation at IJCAI 2023 (the 32nd Int. Joint Conf. on Artificial Intelligence) in Macao. Out of 4566 full-paper submissions, about 15% has been accepted. The paper gives an algorithm for estimating the […]

The paper entitled “On Certificates, Expected Runtimes, and Termination in ProbabilisticPushdown Automata” by Tobias Winkler and Joost-Pieter Katoen has been accepted for presentation at the IEEE/ACM Annual Symposium on Logic on Computer Science 2023 to be held in Boston. The paper studies certification of numerical characteristics of probabilistic pushdown systems, that is, how one can […]

The paper entitled “A Compositional Semantics of Boolean-logic Driven Markov Processes” by Shahid Khan, Joost-Pieter Katoen andMarc Bouissou (EDF) has been accepted as regular paper for IEEE Transactions on Dependable and Secure Computing. This paper provides a compositional and operational semantics (using Markov automata) of BDMPs, a prominent dynamic extension of static fault trees to […]

The proceedings of the 25th Symposium on Formal Methods (FM 2023), edited by Marsha Chechik (Toronto), Joost-Pieter Katoen and Martin Leucker (Lübeck), and published as LNCS volume 14000, are available from March 2 and accessible under: https://link.springer.com/book/10.1007/978-3-031-27481-7.

The project proposal “Probabilistic Model Checking under Partial Observability with Multiple Objectives” (POMPOM) has been granted for funding by the German Research Council. The project aims to develop new model-checking algorithms for combinations of qualitative, stochastic and total expected reward objectives for partially observable Markov decision processes (and games). The funding is for two years […]

The paper entitled “Stochastic Games with Lexicographic Objectives” by Krishnendu Chatterjee (IST Austria), Joost-Pieter Katoen, Stephanie Moor (TU Munich), Maximilian Weininger (Tu Munich), and Tobias Winkler has been accepted for publication in Formal Methods in System Design. This paper presents a detailed study of stochastic turn-based games (SG) with lexicographic objectives. The paper is an […]

Three papers of the MOVES group have been accepted for TACAS 2023! “A Practitioner’s Guide to MDP Model Checking Algorithms” by Arnd Hartmanns, Sebastian Junges, Tim Quatmann and Maximilian Weininger presents an empirical evaluation of various algorithms (different forms of value iteration, policy iteration and direct algorithms) to compute reachability probabilities in Markov decision processes. […]

The paper entitled “A Calculus for Amortized Expected Runtimes” by Kevin Batz, Benjamin Kaminski (Saarland/UCL), Joost-Pieter Katoen, Christoph Matheja (DTU Lyngby) and Lena Verscht has been accepted for presentation at the 50th ACM Symposium on Principles of Programming Languages (POPL). The paper presents a weakest precondition-style calculus to determine the amortized expected run-time of randomized […]

Philipp Schroer and Joost-Pieter Katoen receive a Research Award from WhatsApp, through its parent company, Meta Platforms, Inc. for their research proposal “A Deductive Verification Infrastructure for Probabilistic Programs”. Out of 62 research proposals that were submitted to WhatsApp Privacy Aware Program Analysis, 6 projects have been awarded. For more information, see here.

The paper entitled “Encoding inductive invariants as barrier certificates: synthesis via difference-of-convex programming” by Qiuye Wang, Mingshuai Chen, Bai Xue, Naijun Zhan, and Joost-Pieter Katoen has been accepted for publication in the journal Information and Computation. The paper presents a novel condition on barrier certificates that witnesses unbounded-time safety of differential dynamical systems and provides […]