Write a Blog >>
PLDI 2020
Mon 15 - Fri 19 June 2020

Almost-sure termination is the most basic liveness property of probabilistic programs. We present a novel decomposition-based approach for proving almost-sure termination of probabilistic programs with complex control-flow structure and non-determinism. Our approach automatically decomposes the runs of the probabilistic program into a finite union of ω-regular subsets and then proves almost-sure termination of each subset based on the notion of localized ranking supermartingales. Compared to the lexicographic methods and the compositional methods, our approach does not require a lexicographic order over the ranking supermartingales as well as the so-called unaffecting condition. Thus it has high generality. We present the algorithm of our approach and prove its soundness, as well as its relative completeness. We show that our approach can be applied to some hard cases and the evaluation on the benchmarks of previous works shows the significant efficiency of our approach.

Fri 19 Jun

Displayed time zone: Pacific Time (US & Canada) change

05:00 - 06:00
Probabilistic ProgrammingPLDI Research Papers at PLDI Research Papers live stream
Chair(s): Sasa Misailovic University of Illinois at Urbana-Champaign

YouTube lightning session video

05:00
20m
Talk
Proving Almost-Sure Termination by Omega-Regular Decomposition
PLDI Research Papers
Jianhui Chen Tsinghua University, China, Fei He Tsinghua University, China
05:20
20m
Talk
λPSI: Exact Inference for Higher-Order Probabilistic Programs
PLDI Research Papers
Timon Gehr ETH Zurich, Switzerland, Samuel Steffen ETH Zurich, Switzerland, Martin Vechev ETH Zurich, Switzerland
05:40
20m
Talk
Reactive Probabilistic Programming
PLDI Research Papers
Guillaume Baudart IBM Research, Louis Mandel IBM Research, Eric Atkinson Massachusetts Institute of Technology, USA, Benjamin Sherman Massachusetts Institute of Technology, USA, Marc Pouzet École normale supérieure, Michael Carbin Massachusetts Institute of Technology, USA
DOI Pre-print Media Attached