Mastering Probabilistic Couplings in Relational Program Verification 🖥️

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.