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

POPL-2019-Research-Papers
10:35 - 12:03: Research Papers - Reasoning about Probabilistic Programs at Sala I
Chair(s): Jan HoffmannCarnegie Mellon University
POPL-2019-Research-Papers10:35 - 10:57
Talk
Tetsuya SatoUniversity at Buffalo, SUNY, USA, Alejandro AguirreIMDEA Software Institute, Spain, Gilles BartheIMDEA Software Institute, Marco GaboardiUniversity at Buffalo, SUNY, Deepak GargMax Planck Institute for Software Systems, Justin HsuUniversity of Wisconsin-Madison, USA
Link to publication DOI File Attached
POPL-2019-Research-Papers10:57 - 11:19
Talk
Joseph TassarottiCarnegie Mellon University, Robert Harper
Link to publication DOI File Attached
POPL-2019-Research-Papers11:19 - 11:41
Talk
Kevin BatzRWTH Aachen University, Benjamin Lucien KaminskiRWTH Aachen University; University College London, Joost-Pieter KatoenRWTH Aachen University, Christoph MathejaRWTH Aachen University, Thomas NollRWTH Aachen University
Link to publication DOI File Attached
POPL-2019-Research-Papers11:41 - 12:03
Talk
Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison
Link to publication DOI