Probabilistic coupling for relational reasoning

Tuesday, May 17, 2016 -
12:00pm to 1:00pm

Speaker Name: 

Justin Hsu

Speaker Institution: 

University of Pennsylvania




Probabilistic couplings are a standard mathematical abstraction for reasoning about two distributions. In formal verification, they are often called
probabilistic liftings. While these two concepts are quite related, the
connection has been little explored. In fact, probabilistic couplings and
liftings are a powerful, compositional tool for reasoning about probabilistic
programs. I will give a brief survey of different uses of probabilistic
liftings, and then show how to use these ideas in the relational program logic