Automated Probabilistic Program Analysis

Probabilistic programs are pivotal for cryptography, privacy and quantum programs, are typically a few number of lines, but hard to understand and analyze. The main challenge for their automated analysis is the infinite domain of the program variables combined with the occurrence of parameters. Here, parameters can range over concrete probabilities but can also encompass various aspects of the program, such as number of participants, size of certain variables etc.

McIver and Morgan adapted the seminal Floyd-Hoare proof method to probabilistic programs by making the program annotations real- rather than Boolean-valued expressions in the program variables. Still, the crucial annotations are the loop invariants. The problem to synthesize loop invariants is very challenging for probabilistic programs where real-valued, quantitative invariants are needed.

In this talk, we present a novel approach to synthesize quantitative loop invariants. In order to provide an operational interpretation to the quantitative program annotations, we give a simple operational semantics using parameterized infinite-state Markov decision processes and prove its connection to McIver and Morgan's wp-semantics. Finally, we show the internals of the prototypical tool PRINSYS supporting our invariant-generation approach.