From Couplings to Probabilistic Relational Program Logics
Event details
| Date | 08.06.2018 |
| Hour | 10:15 › 11:00 |
| Location | |
| Category | Conferences - Seminars |
By Justin Hsu
Abstract
Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a variety of probabilistic relational properties.
Bio
Justin Hsu is a post-doctoral researcher at the Cornell University. He obtained his graduate degree from the University of Pennsylvania. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.
More information
Abstract
Many program properties are relational, comparing the behavior of a program (or even two different programs) on two different inputs. While researchers have developed various techniques for verifying such properties for standard, deterministic programs, relational properties for probabilistic programs have been more challenging. In this talk, I will survey recent developments targeting a range of probabilistic relational properties, with motivations from privacy, cryptography, machine learning. The key idea is to meld relational program logics with an idea from probability theory, called a probabilistic coupling. The logics allow a highly compositional and surprisingly general style of analysis, supporting clean proofs for a variety of probabilistic relational properties.
Bio
Justin Hsu is a post-doctoral researcher at the Cornell University. He obtained his graduate degree from the University of Pennsylvania. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms, differential privacy, and game theory.
More information
Practical information
- General public
- Free
Contact
- Host: Laboratory for Automated Reasoning and Analysis, http://lara.epfl.ch