Two papers of the MOVES group have been accepted for the European Symposium on Programming (ESOP) 2026 to be held in Turin, Italy. The paper “Error Localization, Certificates, and Hints for Probabilistic Program Verification via Slicing” by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen presents novel slicing concepts for probabilistic programs, their formalisation and experimental results. More details can be found in the blog post on the Caesar website, including a link to a preprint.

The paper “Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops” by Kevin Batz (UCL), Adrian Gallus, Darion Haase, Benjamin Kaminski (Saarland University),
Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler describes a novel method to compute the exact pushforward of some initial measure through a probabilistic while-loop, based on expressing the semantics of the loop as a fixed point equation on the occupation measure (OM). A sound algorithm is obtained by using generating functions as effective representations of the OM and using a guess/verify heuristic for probabilistic loop invariants.