Talk: Martingale-based Verification of Probabilistic Programs (ONLINE)

LIVE STREAM: https://uwmadison.zoom.us/j/98493278799?pwd=dCszMmtUOCtSYWtHaEVzYUpnWWIxZz09

Abstract: Probabilistic programs extend classical imperative programs with randomization, i.e. the ability to sample a value from a given probability distribution. They provide an expressive framework and have been used in machine learning, network analysis, robotics, randomized algorithms, distributed systems and security. Recent years have seen the development of many probabilistic programming languages such as Church and Pyro. Verifying the correctness of probabilistic programs is often subtler than their non-probabilistic counterparts and problems such as termination and cost analysis require deeper mathematical tools in presence of probabilistic behavior. In this talk, we provide an overview of the martingale-based approach to proving termination and synthesizing cost bounds for probabilistic programs. We then show how martingale-based program analysis can be automated by template-based methods that build upon classical theorems in polyhedral and real algebraic geometry, such as Farkas Lemma, Handelman's Theorem and Putinar's Positivstellensatz. Finally, we provide an overview of remaining challenges and open problems and discuss interesting directions of future work.

Biography: Amir Goharshady is an Assistant Professor of Computer Science and Mathematics at the Hong Kong University of Science and Technology. His research foci include program verification, parameterized algorithms and blockchain. He uses tools from game theory, probability theory, real algebraic geometry and parameterized complexity to tackle diverse problems ranging from data-flow analysis and optimal cache management, to finding termination proofs and resource-usage bounds for probabilistic programs, or quantitatively verifying the security of smart contracts. His research has been supported by the Hong Kong Research Grants Council (RGC), Kaisa, IBM, Meta, the Austrian Academy of Sciences, and the Royal Commission for the Exhibition of 1851 and won three IEEE Larson Best Paper Awards and a Distinguished Paper Award at OOPSLA 2023. He leads the ALPACAS research group (https://amir.goharshady.com/alpacas-research-group) at HKUST.