Algebraic Program Analysis of Probabilistic Programs

The following summary was generated by AI from the slides.

This talk presents an algebraic framework for analyzing probabilistic programs using pre-Markov algebras, which capture sequencing, probabilistic branching, nondeterminism, and conditional choice as first-class algebraic operations. A key technical contribution is a differentiation routine for recursive program schemes over pre-Markov algebras that enables Newton’s method to solve the resulting equation systems, superseding slower Kleene-iteration-based solvers. Preliminary evaluation on reaching-probability and expected-reward analyses demonstrates the approach over programs with loops, recursion, and multiple confluence operations.