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.

Schedule

VeriProp will take place virtually on July 19.

7:00am PDT 16:00 CEST Maria Gorinova Improving inference through program transformations
7:30 - 7:40 Jules Jacobs Paradoxes of Probabilistic Programming
7:40 - 7:50 Dario Stein, Sam Staton Compositional Verification for Probabilistic Programs with Exact Conditioning
7:50 - 8:00 Alexandru Dinu, Sourav Chakraborty, Kuldeep Meel PPCheck: Verifying the Equivalence of Probabilistic Programs
8:10am PDT 17:10 CEST Michael Carbin Programming and reasoning with partial observability
8:40 - 8:50 Wen-Chi Yang, Jean Francois Raskin, Luc De Raedt Lifted Model Checking for Relational MDPs
8:50 - 9:00 Vineet Rajani, Deepak Garg, Gilles Barthe A type-theory for (amortized) expected cost analysis of higher-order probabilistic programs
9:00 - 9:10 Ankush Das, Di Wang, Jan Hoffmann Probabilistic Resource-Aware Session Types
Break
9:30am PDT 18:30 CEST Laura Kovacs Algebra-based Analysis of Polynomial Probabilistic Programs
10:00 - 10:10 Tobias Winkler Weighted Programs and an Application to Almost-Sure Termination
10:10 - 10:20 Martin Helfrich, Javier Esparza, Philipp J. Meyer, Antonin Kucera Verifying Qualitative Liveness Properties of Replicated Systems with Stochastic Scheduling
10:20 - 10:30 Syyeda Zainab, Xiang Chen, Yash Dhamija, Maeve Wildes, Qiyi Tang, Franck van Breugel Probabilistic Model Checking of Randomized Java Code
10:40am PDT 19:40 CEST Guy Van den Broeck Recent Advances in Discrete Probabilistic Program Inference
11:10 - 11:20 Kevin Batz Relatively Complete Verification of Probabilistic Programs
11:20 - 11:30 Holger Hermanns, Michaela Klauck Lab Conditions for Research on Perspicuous Automated Decisions
11:30 - 11:40 Daniel Fremont Scenic: A Language for Scenario Specification and Data Generation

Invited Speakers

Call for Presentations

VeriProP 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 presentations of 10 minutes. 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: Monday, July 5

Notification date: Wednesday, July 7

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

Attending

Please register for the workshop via the official CAV website.

Organization

This workshop will be held on July 19th, 2021, as a satellite event of the 33rd International Conference on Computer-Aided Verification (CAV). The workshop is chaired by: