Static Analysis for Probabilistic Programs: Inferring
Whole Program Properties from Finitely Many Paths
Abstract
We propose an approach for the static analysis of probabilistic programs
that sense, manipulate, and control based on uncertain data.
Examples include programs used in risk analysis, medical decision
making and cyber-physical systems. Correctness properties of
such programs take the form of queries that seek the probabilities
of assertions over program variables. We present a static analysis
approach that provides guaranteed interval bounds on the values
(assertion probabilities) of such queries. First, we observe that for
probabilistic programs, it is possible to conclude facts about the behavior
of the entire program by choosing a finite, adequate set of
its paths.We provide strategies for choosing such a set of paths and
verifying its adequacy. The queries are evaluated over each path
by a combination of symbolic execution and probabilistic volumebound
computations. Each path yields interval bounds that can be
summed up with a coverage bound to yield an interval that encloses
the probability of assertion for the program as a whole. We
demonstrate promising results on a suite of benchmarks from many
different sources including robotic manipulators and medical decision
making programs.