Formally Verifying Randomized Algorithms

Abstract: Probabilistic programs and randomized algorithms play an important role in many leading areas of computer science. While exciting applications expand rapidly, our ability to verify randomized programs lags behind. Like all software, probabilistic programs are susceptible to bugs. Worse, they are hard to check using traditional methods, like testing: the intended behavior is not deterministic, involving a distribution of program behaviors.

In this talk, I will present verification methods for randomized algorithms based on a simple guiding principle: align classical verification methods with the techniques algorithm designers use to prove correctness. In particular, I will discuss how separation logic---a method originally designed for analyzing pointer-manipulating programs---can also model probabilistic independence, giving a new method to prove security of cryptographic protocols. I will also show how verification methods designed for certifying correctness of compiler transformations can also capture a powerful proof technique from probability theory called "proof by coupling", enabling clean verification of properties including privacy of probabilistic queries, incentive compatibility of randomized mechanisms, and stability of learning algorithms.

Bio: Justin Hsu is an assistant professor of Computer Sciences at the University of Wisconsin--Madison. He was a postdoc at Cornell and UCL, after receiving his doctorate in Computer Science from the University of Pennsylvania. His research focuses on formal verification of probabilistic programs, including algorithms from differential privacy, protocols from cryptography, and mechanisms from game theory. His work has been recognized by an NSF CAREER award, a SIGPLAN John C. Reynolds Doctoral Dissertation award, a Facebook TAV award, a Facebook Probability and Programming award, and a Simons Graduate Fellowship in Theoretical Computer Science