Room 206 (2nd floor, badged access)
13 December 2022 - 14h00
Automatic Invariant Generations for Probabilistic Loops
by Ezio Bertocci from TU Wien
Abstract: Probabilistic programs (PPs), originally employed in cryptographic/privacy protocols and randomized algorithms, are now gaining momentum due to the several emerging applications in the areas of machine learning and AI. Probabilistic programming languages include native constructs for sampling distributions allowing to freely mix deterministic and stochastic elements. The resulting flexible framework comes at the price of programs with behaviors hard to analyze, leading to unpredictable adverse consequences in safety-critical applications. One of the main challenges in the analysis of these programs is to compute invariant properties that summarize loop behaviors. Despite recent results, full automation of invariant generation is at its infancy and only targets expected values of the program variables, which is insufficient to recover the full probabilistic program behavior. In this talk, we present some of the results of our project ProbInG that aims at developing novel and fully automated approaches to generate invariants over higher-order moments and the value distribution of program variables, without any user guidance.