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 Times are displayed in time zone: Greenwich Mean Time : Belfast change
10:35 - 12:03: Reasoning about Probabilistic ProgramsResearch Papers at Sala I Chair(s): Jan HoffmannCarnegie Mellon University | |||
10:35 - 10:57 Talk | Formal Verification of Higher-Order Probabilistic Programs Research Papers 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 Media Attached File Attached | ||
10:57 - 11:19 Talk | A Separation Logic for Concurrent Randomized Programs Research Papers Link to publication DOI Media Attached File Attached | ||
11:19 - 11:41 Talk | Quantitative Separation Logic - A Logic for Reasoning about Probabilistic Pointer Programs Research Papers 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 Media Attached File Attached | ||
11:41 - 12:03 Talk | Trace Abstraction Modulo Probability Research Papers Calvin SmithUniversity of Wisconsin - Madison, Justin HsuUniversity of Wisconsin-Madison, USA, Aws AlbarghouthiUniversity of Wisconsin-Madison Link to publication DOI Media Attached |