A Short Introduction to Termination Analysis of Probabilistic Programs
18/04/2022
Speaker
Abstract
Termination is one of the most classical undecidable problems in computer science, going all the way back to Turing's study of the halting problem. Despite its undecidability, it has a central role in formal program verification and a rich body of theory and practical algorithms have been developed over the decades to handle the special decidable cases of this classical problem. In this talk, we first review some of the most prominent and standard ways of proving termination for non-probabilistic programs. We then turn our focus on extending these methods to the much more intricate (and interesting) case of probabilistic programs. We also spend some time on examples showing how and why our intuition fails us when we deal with infinite probability spaces in the context of program analysis.
Bio
Amir Goharshady is an Assistant Professor of Computing and Mathematics at HKUST. His research is in mathematical and algorithmic aspects of program verification and formal methods. He did his PhD at the Institute of Science and Technology Austria (IST Austria) and has been a recipient of various research awards, including fellowships from Facebook, IBM, the Austrian Academy of Sciences, and the Royal Commission for the Exhibition of 1851, as well as the Best PhD Dissertation Awards of the European Association for Programming Languages and Systems (EAPLS) and IST Austria, two IEEE CS Best Student Paper Awards and the Iranian Presidential Research Award (Khwarizmi Prize)