Probabilistic programs are a structured way to describe computations or models with access to some source of randomness. They appear naturally in various safety-, security-, and privacy-critical applications, including randomized algorithms, security protocols, and autonomous systems working in uncertain environments, e.g., due to imprecise sensors.

The behavior of probabilistic programs is often counterintuitive — a consequence of the well-known fact that humans have difficulties reasoning about stochastic processes. In combination with their importance in emerging safety-critical domains, the counterintuitive nature of probabilistic programs means that ensuring their correctness must be based on verification and analysis techniques that are rigorous, tool-supported, and, ideally, largely automated. However, such tools have not kept up with the increasing usage and popularity of probabilistic programs.

In part, the lack of tool support can be explained by the fact that research on probabilistic programs is spread over multiple fields. In addition to the classical understanding of probabilistic programs as randomized algorithms, probabilistic programs have received rapidly increasing attention as a modeling formalism for complex probability distributions in machine learning, artificial intelligence, and cognitive science.

This workshop will provide a forum for research on the automated verification of probabilistic systems that are in some way described by a programming language, with a particular focus on both symbolic methods and compositional approaches.

Invited Speakers

Preliminary Program

Time Author(s) Title
9:00 Justin Hsu Type Systems for Exchangeability
9:45 Krishnendu Chatterjee, Ehsan Kafshdar Goharshady and Đorđe Žikelić SuperDP: Differential Privacy Refutation via Supermartingales
10:00 Éléanore Meyer and Jürgen Giesl Deciding Termination of Simple Randomized Loops
10:15 Jan-Christoph Kassing, Arion Scheid, Henri Nagel and Jürgen Giesl A First Decision Procedure for Almost-Sure Termination of Probabilistic Term Rewriting
10:30   Coffee Break
11:00 Fabian Zaiser How to Verify Probabilistic Inference — and What That Even Means
11:45 Darion Haase, Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler Generating Functions Meet Occupation Measures: Invariant Synthesis for Probabilistic Loops
12:00 Sebastian Körner Unbounded Nondeterministic Choice in Weighted Programs
12:15 Uddalok Sarkar, Sourav Chakraborty, Kuldeep S. Meel Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
12:30   Lunch (Provided)
14:00 Milan Ceska Coupling Verification and Learning for Safe and Explainable Decision-Making under Uncertainty
14:45 Kittiphon Phalakarn and Ichiro Hasuo Value Iteration for Stochastic Parity Games
15:00 Takuma Monma, Clovis Eberhart and Hiroshi Unno Probabilistic Loop Acceleration via a Quantitative Fixpoint Logic
15:15 Satoshi Kura and Hiroshi Unno A Hierarchy of Supermartingales for ω-Regular Verification
15:30   Coffee Break
16:00 Suguman Bansal Specification-Guided Reinforcement Learning
16:45 David Richter, Timon Böhler, Benedict Smit, Pascal Weisenburger and Mira Mezini Verified Inverse Function Search for Normalizing Flows
17:00 Romin Doz, Christin Matheja, Francesca Meneghello, Laura Nenzi, Andrey Rivkin and Simone Silvetti Analytical Inference for Business Processes with Uncertainties via Probabilistic Programming

Call for Presentations

VeriProP 2026, co-located with CAV, aims to bring together researchers interested in the tool-supported verification of probabilistic programs, models, and systems. This includes probabilistic model checking, program verification in the presence of a source of randomness, or formal guarantees for statistical machine learning algorithms and artificial intelligence systems.

We solicit contributed short presentations. Topics of interest include, but are not limited to:

We call for extended abstracts (1-2 pages in pdf format) describing either ongoing research or an overview of past research in the workshop’s scope. We welcome abstracts covering work that has been previously published or is currently under review. There will be no formal proceedings.

Submission

Submission deadline: May 6th 2026 AoE May 21st 2026 AoE

Submission link: https://submissions.floc26.org/veriprop/

Attending

The workshop will take place on July 25th.

Organization

The workshop is chaired by:

Steering committee:

Previous Editions