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.

“Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants” by Kevin Batz, Mingshuai Chen, Sebastian Junges, Benjamin Lucien Kaminski, Joost-Pieter Katoen and Christoph Matheja presents a CEGIS-based approach to synthesize inductive invariants for probabilistic programs.

“Certificates for Probabilistic Pushdown Automata via Optimistic Value Iteration” by Tobias Winkler and Joost-Pieter Katoen addresses the verification problem for probabilistic pushdown automata, where the goal is not just to establish whether some property holds but also to provide a proof that can be easily checked (a certificate).