PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs
Automatically establishing that a probabilistic program satisfies some property $\varphi$ is a challenging problem. While a sampling-based approach—which involves running the program repeatedly—can suggest that $\varphi$ holds, to establish that the program satisfies $\varphi$, analysis techniques must be used. Despite recent successes, probabilistic static analyses are still more difficult to design and implement than their deterministic counterparts. This paper presents a framework, called PMAF, for designing, implementing, and proving the correctness of static analyses of probabilistic programs with challenging features such as recursion, unstructured control-flow, divergence, nondeterminism, and continuous distributions. PMAF introduces pre-Markov algebras to factor out common parts of different analyses. To perform interprocedural analysis and to create procedure summaries, PMAF extends ideas from non-probabilistic interprocedural dataflow analysis to the probabilistic setting. One novelty is that PMAF is based on a semantics formulated in terms of a control-flow hyper-graph for each procedure, rather than a standard control-flow graph. To evaluate its effectiveness, PMAF has been used to reformulate and implement existing intraprocedural analyses for Bayesian-inference and the Markov decision problem, by creating corresponding interprocedural analyses. Additionally, PMAF has been used to implement a new interprocedural linear expectation-invariant analysis. Experiments with benchmark programs for the three analyses demonstrate that the approach is practical.
Thu 21 JunDisplayed time zone: Eastern Time (US & Canada) change
16:10 - 17:00 | Analyzing Probabilistic ProgramsPLDI Research Papers at Grand Ballroom CD Chair(s): Eva Darulova MPI-SWS | ||
16:10 25mTalk | Bounded Expectations: Resource Analysis for Probabilistic Programs PLDI Research Papers Van Chan Ngo Carnegie Mellon University, Quentin Carbonneaux Yale University, Jan Hoffmann Carnegie Mellon University Media Attached | ||
16:35 25mTalk | PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs PLDI Research Papers Di Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Media Attached |