Probabilistic Program Analysis using Martingale Theory


August 13, 2013


Sriram Sankaranarayanan


University of Colorado Boulder


Probabilistic programs are standard imperative programs enriched with constructs to generate random values according to a pre-specified distribution. Such programs are common in a variety of application domains, including risk assessment, biological systems, sensor fusion algorithms and randomized algorithms. We present deductive 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 martingales and super martingales from probability theory.
First, we define the concept of (super) martingales for loops in probabilistic programs, and present analogies between super martingales and inductive invariants. We then use 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. Using the notion of a super martingale ranking function (SMRF), we prove almost sure termination of probabilistic programs. We extend constraint-based approaches for synthesizing inductive invariants to also synthesize martingales and super-martingale ranking functions for probabilistic programs. We present some applications of our approach to reason about invariance and termination of some probabilistic program benchmarks.
Joint work with Aleksandar Chakarov, University of Colorado Boulder.


Sriram Sankaranarayanan

Sriram Sankaranarayanan is an assistant professor of Computer Science at the University of Colorado, Boulder. His research interests include automatic techniques for reasoning about the behavior of computer and cyber-physical systems. Sriram obtained a PhD in 2005 from Stanford University where he was advised by Zohar Manna and Henny Sipma. Subsequently he worked as a research staff member at NEC research labs in Princeton, NJ. He has been on the faculty at CU Boulder since 2009. Sriram has been the recipient of awards including
the President’s Gold Medal from IIT Kharagpur (2000), Siebel Scholarship (2005), the CAREER award from NSF (2009) and the Dean’s award for outstanding junior faculty for the College of Engineering at CU Boulder (2012).