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

Program

Time Author(s) Title
9:00 Alejandro Aguirre A Resource-Based Approach to Probabilistic Program Verification
9:45 Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný and Đorđe Žikelić Refuting Equivalence in Probabilistic Programs with Conditioning
10:00 Niki Omidvari, Fredrik Dahlqvist Symbolically Evaluating Probabilistic Programs Using Cylindrical Algebraic Decomposition
10:15 Diptarko Roy, Mirco Giacobbe, Alessandro Abate Probabilistic Omega-Regular Verification with Supermartingales
10:30   Coffee Break
11:00 Anne-Kathrin Schmuck TBA
11:45 Kittiphon Phalakarn, Yun Chen Tsai, Ichiro Hasuo Widest Path Games and Maximality Inheritance in Bounded Value Iteration for Stochastic Games
12:00   Lunch (provided)
14:00 Stefan Kiefer Strategies in Infinite Stochastic Systems
14:45 Filip Macák, Roman Andriushchenko, Milan Češka, Sebastian Junges PAYNT: A Framework for Controller Synthesis Under Uncertainty
15:00 Bahare Salmani, Vincent Derkinderen Relating Probabilistic Model Checking and Weighted Model Counting
15:15 Yun Chen Tsai, Kittiphon Phalakarn, S. Akshay, Ichiro Hasuo Chance and Mass Interpretations of Probabilities in Markov Decision Processes
15:30   Coffee Break
16:00 Francesca Randone TBA
16:45 Luko van der Maas, Sebastian Junges Learning Verified Monitors for Hidden Markov Models
17:00 Francesco Pontiggia, Ezio Bartocci, Michele Chiari Exact Inference for Nested Discrete Probabilistic Programs

Call for Presentations

VeriProP 2025, 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 9th 23rd, 2025 AOE

Submission link: https://easychair.org/conferences/?conf=veriprop2025

Attending

The workshop will take place on July 22rd, the day before CAV. Please register via the official CAV website.

Travel Funding

Students who are giving a contributed presentation may apply for travel funding by contacting Fredrik Dahlqvist. Since the available budget is limited, we kindly ask students to apply only if they cannot fund their trip by any other means.

Organization

The workshop is chaired by:

Steering committee:

Previous Editions