279 citations · 1.4k across the 46 of their papers we have counts for
7 papers · 1 filter
Probabilistic Couplings for Probabilistic Reasoning
Justin Hsu
This thesis explores proofs by coupling from the perspective of formal verification. Long employed in probability theory and theoretical computer science, these proofs construct co…
Approximate Span Liftings
Tetsuya Sato, Gilles Barthe, Marco Gaboardi +2
We develop new abstractions for reasoning about relaxations of differential privacy: Rényi differential privacy, zero-concentrated differential privacy, and truncated concentrated…
Synthesizing Coupling Proofs of Differential Privacy
Aws Albarghouthi, Justin Hsu
Differential privacy has emerged as a promising probabilistic formulation of privacy, generating intense interest within academia and industry. We present a push-button, automated…
Proving Expected Sensitivity of Probabilistic Programs
Gilles Barthe, Thomas Espitau, Benjamin Grégoire +2
Program sensitivity, also known as Lipschitz continuity, describes how small changes in a program's input lead to bounded changes in the output. We propose an average notion of pro…
Relational -Liftings for Differential Privacy
Gilles Barthe, Thomas Espitau, Justin Hsu +2
Recent developments in formal verification have identified approximate liftings (also known as approximate couplings) as a clean, compositional abstraction for proving differential…
A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +2
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical syste…
Proving uniformity and independence by self-composition and coupling
Gilles Barthe, Thomas Espitau, Benjamin Grégoire +2
Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chai…