Martingales for Probabilistic Termination and Safety

Probabilistic programs (PPs) are programs written in some general-purpose programming language enriched with probabilistic constructs, such as sampling of a variable value from a probability distribution. PPs emerge in a variety of application domains, including machine learning, security, or network design, to name a few. To ensure that systems developed in these domains are safe and reliable, it is desirable to develop formal verification techniques for proving properties of PPs. In this talk, we will survey recent advances in analysis of probabilistic programs, focusing on techniques built on the concept of martingales from probability theory.