Trace Abstraction Modulo Probability
Abstract
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 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: we use program synthesis methods to select axioms for sampling instructions, and then apply Craig interpolation to prove that traces fail the target specification with only a small probability. Our method 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 automatically establish accuracy properties of these algorithms.
Cite
@article{arxiv.1810.12396,
title = {Trace Abstraction Modulo Probability},
author = {Calvin Smith and Justin Hsu and Aws Albarghouthi},
journal= {arXiv preprint arXiv:1810.12396},
year = {2018}
}