Open for all UnRAVeL Members: MOVES Seminar: Marcel Moosbrugger: Probabilistic Program Analysis using Algebraic Recurrences

Thursday, January 27, 2022, 11:00am

Location: Hybrid

Speaker: Marcel Moosbrugger

 

Abstract:

Probabilistic programs (PPs) are common imperative programs extended with the capability of sampling from probability distributions. Due to their probabilistic nature, the automated analysis of PPs is hard. As in traditional program analysis, loops are the main obstacle for automated approaches. In the first 1.5 years of my doctoral studies, I developed techniques based on linear recurrences to (1) automatically analyze the termination behavior of probabilistic loops and (2) automatically derive invariants over higher moments of probabilistic loop variables.

Invariants over variable moments can be used to further bound tail probabilities and to approximate the probability distributions of program variables in any loop iteration. The theoretical results led to two tools (1) Amber, a tool for automated termination analysis of PPs, and (2) XYZ (under double-blind review) for deriving invariants over moments of program variables and further analysis using these invariants. In the talk, I will give an overview of the theoretical techniques using linear recurrences for PP analysis as well as a demonstration of Amber and XYZ.