The two papers “Verifying Sampling Algorithms via Distributional Invariants” by Kevin Batz (University College London), Joost-Pieter Katoen, Tobias Winkler and Daniel Zilken and “Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops” by Kevin Batz (University College London), Adrian Gallus, Darion Haase, Benjamin Kaminski (Saarland University and University College London), Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler have been accepted at the workshop on Languages for Inference 2026 (LAFI 2026).

The first paper presents a Hoare-like verication framework for verifying partial and total correctness of discrete probabilistic programs. The framework is applied to two non-trivial sampling algorithms: the Fast Dice Roller and the Fast Loaded Dice Roller.

The second paper addresses exact automatic loop analysis for discrete probabilistic loops with a given discrete initial distribution over program states and presents a heuristic template-based invariant synthesis technique. This is obtained by combining generating functions as a representation for (infinite-support) distributions with a characterization of a loop’s output distribution through its occupation measure due to Sharir et al.