Skip to the content.

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.

Program

Time Authors Title
9:00 Erika Abraham TBA
9:50 Kittiphon Phalakarn, Toru Takisaka, Thomas Haas and Ichiro Hasuo Widest Paths and Global Propagation in Bounded Value Iteration for Stochastic Games
10:10 Thom Badings, Alessandro Abate, Nils Jansen, Dave Parker, Hasan Poonawala, Licio Romao and Marielle Stoelinga Safe Sampling-Based Planning for Stochastic Systems with Uncertain Dynamics
10:30 Coffee break  
11:00 Kuldeep Meel TBA
11:50 Phillipp Schroer A Quantitative Verification Infrastructure
12:10 Fabian Meyer, Marcel Hark and Jürgen Giesl Inferring Expected Runtimes and Sizes
12:30 Lunch break  
14:00 Andrzej Wasowski Quantifying Leakage in Privacy Risk Analysis using Probabilistic Programming
14:50 William Smith, Alexandra Silva and Fredrik Dahlqvist Deterministic stream-sampling for probabilistic programming: semantics and verification
15:10 Wojciech Rozowski, Tobias Kappé, Todd Schmid and Alexandra Silva Probabilistic Guarded Kleene Algebra with Tests
15:30 Coffee break  
16:00 Sylvie Putot TBA
16:50 Lutz Klinkenberg Verifying Probabilistic Programs using Generating Functions
17:10 Closing  

Call for Presentations

VeriProP 2022, co-located with CAV and the federated logic conference, 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 are excited to have 4 invited speakers covering a range of perspectives:

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 date: May 10 May 23

Notification date: June 15

Submission link: easychair.org/my/conference?conf=veriprop2022

Attending

The workshop will take place on August 12, the second day after CAV. Please register via the official FloC website.

Organization

This workshop will be held as a satellite event of FLoC 2022. The workshop is chaired by: