Towards Analysis of Sequential Probabilistic Programs: Invariant Generation

In this talk we look at the analysis of sequential probabilistic programs written in pGCL. First, we introduce an intuitive operational semantics in terms of a reward MDP and show how this is related to the expectation transformer semantics used by McIver and Morgan. After that, ongoing work in analysis of pGCL programs is presented. In particular proofs of the expected outcome of a program rely on invariants which are hard to find. Our goal is to push the bounds of automation and assist the generation of invariants that can be used such proofs.