PMAF: An Algebraic Framework for Static Analysis of Probabilistic Programs
Di Wang, Jan Hoffmann, and Thomas Reps
Automatically establishing that a probabilistic program satisfies
some property φ is a challenging problem.
While a sampling-based approach—which involves running the program
repeatedly—can suggest that φ holds, to establish that
the program satisfies φ, 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.
(Click here to access the paper:
PDF.)