Probabilistic Program Analysis Using Martingales

Aleksandar Chakarov and Sriram Sankaranarayanan
We present techniques for the analysis of infinite state probabilistic programs to synthesize probabilistic invariants and prove almost-sure termination. Our analysis is based on the notion of (super) martingales from probability theory. First, we define the concept of (super) martingales for loops in probabilistic 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.
Computer-Aided Verification (CAV 2013) (to appear).
Note: Copyright belongs to the publisher Springer-Verlag. We have posted a copy of your paper for personal use only.

Sriram Sankaranarayanan