The following three papers have been accepted for the 27th Symposium on Formal Methods (2026) in Tokyo, Japan:

(1) Tools and Algorithms for Sound Multi-Objective Probabilistic Model Checking by Arnd Hartmanns (U. Twente), Tim Quatmann and Mark van Wijk (U. Twente). This paper introduces tools for approximating multi-objective probabilistic model checking for Markov decision processes (MDPs) via a process of over- and under-approximation that converges towards sound results.

(2) Verifying Sampling Algorithms via Distributional Invariants by Daniel Zilken, Kevin Bath (Cornell), Joost-Pieter Katoen and Tobias Winkler. This paper shows how the correctness of discrete sampling algorithms can be shown effectively using distributional invariants, a concept originating from MDP verification that is lifted to programs.

(3) Highly Incremental: A Simple Programmatic Approach for Many Objectives by Philipp Schröer and Joost-Pieter Katoen. This paper introduces a reward command to a probabilistic programming language, and shows how it can be used, in conjunction with ghost variables, to enable reasoning about a range of quantitative properties using standard weakest pre-expectation semantics.