154 citations · 897 across the 34 of their papers we have counts for
5 papers · 1 filter
Coupling proofs are probabilistic product programs
Gilles Barthe, Benjamin Grégoire, Justin Hsu +1
Couplings are a powerful mathematical tool for reasoning about pairs of probabilistic processes. Recent developments in formal verification identify a close connection between coup…
Advanced Probabilistic Couplings for Differential Privacy
Gilles Barthe, Noémie Fong, Marco Gaboardi +3
Differential privacy is a promising formal approach to data privacy, which provides a quantitative bound on the privacy cost of an algorithm that operates on sensitive information.…
Synthesizing Probabilistic Invariants via Doob's Decomposition
Gilles Barthe, Thomas Espitau, Luis María Ferrer Fioriti +1
When analyzing probabilistic computations, a powerful approach is to first find a martingale---an expression on the program variables whose expectation remains invariant---and then…
A program logic for union bounds
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire +2
We propose a probabilistic Hoare logic aHL based on the union bound, a tool from basic probability theory. While the union bound is simple, it is an extremely common tool for analy…
Proving Differential Privacy via Probabilistic Couplings
Gilles Barthe, Marco Gaboardi, Benjamin Grégoire +2
In this paper, we develop compositional methods for formally verifying differential privacy for algorithms whose analysis goes beyond the composition theorem. Our methods are based…