Name
Abstract | ||
|---|---|---|
Proof by coupling is a classical proof technique for establishing probabilistic properties of two probabilistic processes, like stochastic dominance and rapid mixing of Markov chains. More recently, couplings have been investigated as a useful abstraction for formal reasoning about relational properties of probabilistic programs, in particular for modeling reduction-based cryptographic proofs and for verifying differential privacy. In this paper, we demonstrate that probabilistic couplings can be used for verifying non-relational probabilistic properties. Specifically, we show that the program logic pRHL---whose proofs are formal versions of proofs by coupling---can be used for formalizing uniformity and probabilistic independence. We formally verify our main examples using the EasyCrypt proof assistant. |
Year | Venue | DocType |
|---|---|---|
2017 | LPAR | Conference |
Volume | Citations | PageRank |
abs/1701.06477 | 6 | 0.44 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Gilles Barthe | 1 | 2337 | 152.36 |
| Thomas Espitau | 2 | 6 | 0.44 |
| Benjamin Grégoire | 3 | 817 | 48.93 |
| Justin Hsu | 4 | 364 | 24.38 |
| Pierre-Yves Strub | 5 | 540 | 29.87 |