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
- Sam Staton (University of Oxford): Semantics and types for non-parametric probabilistic programming
- Christel Baier (TU Dresden): Probability-raising Causality in Markov Decision Processes
- Djordje Zikelic (ISTA): From Probabilistic Program Analysis to Learning-based Stochastic Control with Martingales
- Raphaëlle Crubillé (CNRS / Aix-Marseille Université): TBA
Program
| Time | Author(s) | Title |
|---|---|---|
| 9:00 | Opening | |
| 9:15 | Sam Staton | Semantics and types for non-parametric probabilistic programming |
| 10:00 | Nikolai Käfer | Semantics for Cyclic Bayesian Networks |
| 10:15 | Mateo Torres-Ruiz, Robin Piedeleu, Alexandra Silva and Fabio Zanasi | On Iteration in Discrete Probabilistic Programming |
| 10:30 | Coffee break | |
| 11:00 | Đorđe Žikelić | From Probabilistic Program Analysis to Learning-based Stochastic Control with Martingales |
| 11:45 | Ichiro Hasuo | Compositionality in Probabilistic Verification, Statistical Inference, and Stochastic Optimization |
| 12:00 | Milan Ceska, Roman Andriushchenko and Sebastian Junges | PAYNT: A Tool for Inductive Synthesis of Probabilistic Programs |
| 12:15 | Edward Kim, Jay Shenoy, Sebastian Junges, Daniel Fremont, Alberto Sangiovanni-Vincentelli and Sanjit Seshia | Querying Labelled Data with Probabilistic Programs for Sim-to-Real Validation |
| 12:30 | Lunch break | |
| 14:00 | Christel Baier | Probability-raising Causality in Markov Decision Processes |
| 14:45 | Eric Atkinson, Ellie Y. Cheng, Guillaume Baudart, Louis Mandel and Michael Carbin | Verifying Performance Properties of Probabilistic Inference |
| 15:00 | William Smith and Fredrik Dahlqvist | Construction and verification of infinite-dimensional samplers |
| 15:15 | Tobias Gürtler and Benjamin Kaminski | Belief Programming in Probabilistic Environments |
| 15:30 | Coffee break | |
| 16:00 | Raphaëlle Crubillé | Symbolic protocol verification with dice: process equivalences in the presence of probabilities |
| 16:45 | Alejandro Aguirre, Christoph Matheja and Philipp Schröer | Towards Automated Verification of Expected Sensitivity in Caesar |
| 17:00 | Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti and Lars Birkedal | Asynchronous Probabilistic Couplings in Higher-Order Separation Logic |
| 17:15 | Closing |
Call for Presentations
VeriProP 2023, 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:
- Symbolic approaches to the verification of Markov models
- Exact inference techniques
- Abstract interpretation for probabilistic programs
- Domain-specific probabilistic programming languages
- Verification of inference algorithms
- Automation of deductive approaches to verifying probabilistic programs-
- Probabilistic program reasoning in safety, security, or privacy
- Synthesis of probabilistic programs
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 9 May 19
Submission link: https://easychair.org/my/conference?conf=veriprop2023
Attending
The workshop will take place on July 17, the day after CAV. Please register via the official CAV website.
Organization
The workshop is chaired by:
- Michele Chiari, TU Wien
- Fredrik Dahlqvist, Queen Mary University of London
- Sebastian Junges, Radboud University
- Benjamin Kaminski, Saarland University and University College London
- Christoph Matheja, Technical University of Denmark