MPI-INF Logo
Campus Event Calendar

Event Entry

What and Who

Randomized Algorithms Meets Formal Verification

Justin Hsu
University of Pennsylvania
SWS Colloquium

Justin Hsu is a final year graduate student in Computer Science at the University of Pennsylvania. He obtained his undergraduate degree in Mathematics
from Stanford University. His research interests span formal verification and theoretical computer science, including verification of randomized algorithms,
differential privacy, and game theory. He is the recipient of a Simons graduate fellowship in Theoretical Computer Science.
SWS, RG1, MMCI  
AG Audience
English

Date, Time and Location

Wednesday, 8 March 2017
10:00
90 Minutes
E1 5
029
Saarbrücken

Abstract

Algorithms and formal verification are two classical areas of computer science. The two fields apply rigorous mathematical proof to seemingly disparate ends---on the one hand, analyzing computational efficiency of algorithms; on the other, designing techniques to mechanically show that programs are correct.

In this talk, I will present a surprising confluence of ideas from these two areas. First, I will show how coupling proofs, used to analyze random walks and Markov chains, correspond to proofs in the program logic pRHL (probabilistic Relational Hoare Logic). This connection enables formal verification of novel probabilistic properties, and provides an structured understanding of proofs by coupling. Then, I will show how an approximate version of pRHL, called apRHL, points to a new, approximate version of couplings closely related to differential privacy. The corresponding proof technique---proof by approximate coupling---enables cleaner proofs of differential privacy, both for humans and for formal verification. Finally, I will share some directions towards a possible "Theory AB", blending ideas from both worlds.

Contact

Claudia Richter
9303 9103
--email hidden

Video Broadcast

Yes
Kaiserslautern
G26
111
passcode not visible
logged in users only

Uwe Brahm, 03/06/2017 17:31
Claudia Richter, 02/10/2017 11:09 -- Created document.