Presenter: Mingqi Yang
Authors: Aleksandar Chakarov, University of Colorado; Sriram Sankaranarayanan, University of Colorado
Abstract: We present techniques for the analysis of infinite state probabilistic programs to synthesize probabilistic invariants and prove almost-sure termina tion. Our analysis is based on the notion of (super) martingales from probability theory. First, we define the concept of (super) martingales for loops in probabilis tic programs. Next, we present the use of concentration of measure inequalities to bound the values of martingales with high probability. This directly allows us to infer probabilistic bounds on assertions involving the program variables. Next, we present the notion of a super martingale ranking function (SMRF) to prove almost sure termination of probabilistic programs. Finally, we extend constraint-based techniques to synthesize martingales and super-martingale ranking functions for probabilistic programs. We present some applications of our approach to reason about invariance and termination of small but complex probabilistic programs.
URL: https://link.springer.com/chapter/10.1007/978-3-642-39799-8_34