Skip to main content

Automated Probabilistic Program Analysis

Joost-Pieter Katoen ( RWTH Aachen University, Germany )

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.

Speaker bio

Joost-Pieter Katoen is distinguished professor at the RWTH Aachen University, Germany, and part-time associated with the University of Twente, the Netherlands. His research focuses on the foundations of software modeling and veri fication with an emphasis on quantitative system aspects. Together with Christel Baier, he authored the book "Principles of Model Checking". He is member of IFIP WGs 1.8 and 2.2, and chairs the steering committees of ETAPS and QEST.

Share this: