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
Times are displayed in time zone: Pacific Time (US & Canada) change

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

YouTube lightning session video

05:00 - 05:20
PLDI Research Papers
Jianhui ChenTsinghua University, China, Fei HeTsinghua University, China
05:20 - 05:40
PLDI Research Papers
Timon GehrETH Zurich, Switzerland, Samuel SteffenETH Zurich, Switzerland, Martin VechevETH Zurich, Switzerland
05:40 - 06:00
PLDI Research Papers
Guillaume BaudartIBM Research, Louis MandelIBM Research, Eric AtkinsonMassachusetts Institute of Technology, USA, Benjamin ShermanMassachusetts Institute of Technology, USA, Marc PouzetÉcole normale supérieure, Michael CarbinMassachusetts Institute of Technology, USA
DOI Pre-print Media Attached