CS Talk
Justin Hsu, University of Pennsylvania
Title: Randomized Algorithms Meets Formal Verification
Host: Joan Feigenbaum
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. 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, and a new kind of proof by approximate coupling. The corresponding proof technique 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.
Bio
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.