Relational Program Verification and Probabilistic Couplings - Gilles Barthe

Workshop on Software Correctness and Reliability 2016 Probabilistic couplings are a powerful tool for analyzing the convergence of probabilistic processes. Recently, it has been observed that probabilistic couplings are closely tied to probabilistic relational Hoare logics which have been used to reason about computational security of cryptographic constructions and differential privacy of data-mining algorithms. I will introduce couplings and outline its connection with probabilistic relational program logics, and present recent developments that further leverage this connection.