Algorithms consume our personal data and make decisions that affect our lives. How can we make sure that these algorithms do not leak our private data? How do we make sure they are fair? Over the past few years, we have been exploring this question through the lens of automated verification and synthesis. In this talk, I will discuss automated techniques for proving the correctness of randomized algorithms and apply them to differentially private mechanisms, which have seen numerous applications in privacy-preserving data analysis as well as ensuring forms of fairness in decision-making. Technically, I will demonstrate how powerful SMT solvers, which revolutionized automated verification of traditional programs, can be applied to reasoning about randomized algorithms.
Aws Albarghouthi is an assistant professor at the University of Wisconsin-Madison. He studies automated synthesis and verification of programs, recently with an eye on socially sensitive programs and properties, including fair decision-making, private data analysis, and socially aware robots. He received his PhD from the University of Toronto. He has received a number of best-paper awards for his work (at FSE, UIST, and FAST), an NSF CAREER award, a Google Faculty Research Award, and a Facebook Research Award.