PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs

The following summary was generated by AI from the slides.

PMAF is an algebraic dataflow-analysis framework for first-order probabilistic programs that models programs as control-flow hypergraphs and derives equation systems whose elements live in a pre-Markov algebra capturing sequencing, probabilistic choice, and nondeterminism. The framework recovers two existing analyses — Bayesian inference via distribution-transformer matrices and Markov decision problems via real-valued reward gain — as instantiations, and introduces a novel interprocedural linear expectation-invariant analysis using a relational polyhedral domain. A prototype implementation matches or improves on hand-derived expectation invariants across benchmarks drawn from the literature, with runtimes under one second per program.