Thu 21 Jun 2018 16:35 - 17:00 at Grand Ballroom CD - Analyzing Probabilistic Programs Chair(s): Eva Darulova

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 Jun

16:10 - 17:00: PLDI Research Papers - Analyzing Probabilistic Programs at Grand Ballroom CD
Chair(s): Eva DarulovaMPI-SWS
pldi-2018-papers16:10 - 16:35
Van Chan NgoCarnegie Mellon University, Quentin CarbonneauxYale University, Jan HoffmannCarnegie Mellon University
Media Attached
pldi-2018-papers16:35 - 17:00
Di WangCarnegie Mellon University, Jan HoffmannCarnegie Mellon University, Thomas RepsUniversity of Wisconsin - Madison and GrammaTech, Inc.
Media Attached