In this talk, we will describe progress on computing invariants involving expected values of program variables in probabilistic programs that combine imperative programs with random number generation constructs. Such invariants can express properties such as “for any loop iteration, the average value of x is less than the average of y”. We will first examine a proof system for such invariants, culminating in a fixed point characterization. We then show how such fixed points can indeed be computed using abstract interpretation, presenting a prototype static analysis that realizes our ideas using the polyhedral abstract domain. We conclude by examining connections between our fixed points and concepts in martingale theory.

Joint work with Aleksandar Chakarov.