Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Wed 16 Jan 2019 11:41 - 12:03 at Sala I - Reasoning about Probabilistic Programs Chair(s): Jan Hoffmann

We propose trace abstraction modulo probability, a proof technique for verifying high-probability accuracy guarantees of probabilistic programs. Our proofs overapproximate the set of program traces using the new notion of failure automata, finite-state automata that upper bound the probability of failing to satisfy a target specification. We automate proof construction by reducing probabilistic reasoning to logical reasoning: (i) we exploit program synthesis methods to select and instantiate axioms about sampling instructions, and then (ii) utilize Craig interpolation to show that traces failing the target specification occur with small probability. Our logical method naturally handles programs with unknown inputs, parameterized distributions, infinite state spaces, and parameterized specifications. We evaluate our technique on a range of randomized algorithms drawn from the differential privacy literature and beyond. To our knowledge, our approach is the first to be able to automatically establish accuracy properties of such sophisticated algorithms.

Wed 16 Jan

Displayed time zone: Belfast change

10:35 - 12:03
Reasoning about Probabilistic ProgramsResearch Papers at Sala I
Chair(s): Jan Hoffmann Carnegie Mellon University
10:35
22m
Talk
Formal Verification of Higher-Order Probabilistic Programs
Research Papers
Tetsuya Sato University at Buffalo, SUNY, USA, Alejandro Aguirre IMDEA Software Institute, Spain, Gilles Barthe IMDEA Software Institute, Marco Gaboardi University at Buffalo, SUNY, Deepak Garg Max Planck Institute for Software Systems, Justin Hsu University of Wisconsin-Madison, USA
Link to publication DOI Media Attached File Attached
10:57
22m
Talk
A Separation Logic for Concurrent Randomized Programs
Research Papers
Joseph Tassarotti Carnegie Mellon University, Robert Harper
Link to publication DOI Media Attached File Attached
11:19
22m
Talk
Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs
Research Papers
Kevin Batz RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University; University College London, Joost-Pieter Katoen RWTH Aachen University, Christoph Matheja RWTH Aachen University, Thomas Noll RWTH Aachen University
Link to publication DOI Media Attached File Attached
11:41
22m
Talk
Trace Abstraction Modulo Probability
Research Papers
Calvin Smith University of Wisconsin - Madison, Justin Hsu University of Wisconsin-Madison, USA, Aws Albarghouthi University of Wisconsin-Madison
Link to publication DOI Media Attached