Lecture: Invariance and Termination Analysis for Probabilistic Programs, Jan. 16

Download and share the flier

Invariance and Termination Analysis for Probabilistic Programs
Sriram Sankaranarayanan, assistant professor
Department of Computer Science, University of Colorado at Boulder

Thursday, January 16, 2014
noon–1 p.m.
Brickyard (BYENG) 510 [map]

Abstract:
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. Sriram Sankaranarayanan will present deductive techniques for the analysis of infinite state probabilistic programs to synthesize probabilistic “invariants” and prove almost-sure termination. The analysis is based on the notion of martingales and super martingales from probability theory.

First, Sankaranarayanan define the concept of (super) martingales for loops in probabilistic programs, and present analogies between super martingales and inductive invariants. The researchers then use concentration of measure inequalities to bound the values of martingales with high probability. This directly allows them to infer probabilistic bounds on assertions involving the program variables. Using the notion of a super martingale ranking function (SMRF), they prove almost sure termination of probabilistic programs. They extend constraint-based approaches for synthesizing inductive invariants to also synthesize martingales and super-martingale ranking functions for probabilistic programs. Sankaranarayanan will 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.

BIO
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 Ph.D. 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). Learn more at www.cs.colorado.edu/~srirams

Hosted by Professor Georgios Fainekos