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 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:1025mTalk Bounded Expectations: Resource Analysis for Probabilistic ProgramsPLDI Research PapersVan Chan Ngo Carnegie Mellon University, Quentin Carbonneaux Yale University, Jan Hoffmann Carnegie Mellon University Media Attached 16:3525mTalk PMAF: An Algebraic Framework for Static Analysis of Probabilistic ProgramsPLDI Research PapersDi Wang Carnegie Mellon University, Jan Hoffmann Carnegie Mellon University, Thomas Reps University of Wisconsin - Madison and GrammaTech, Inc. Media Attached