Our paper, “Bounded Expectations: Resource Analysis for Probabilistic Programs” (with Quentin Carbonneaux and Jan Hoffmann), will appear in the 2018 Programming Language Design and Implementation (PLDI). The paper and technical report can be obtained here. The associated tool, Absynth, is also provided.
This work presents the first static analyzer for deriving symbolic polynomial bound on the expected value of resource usage such as runing time, memory allocation, and energy consumption of (imperative) probabilistic programs.
Probabilistic programing languages are standard programming languages like C, Java, or ML, with two additional constructs:
The sampling construct for drawing a value at random from probability distributions
The probabilistic branching construct for controlling the flow in a program through observations.
The applications of probabilistic programming is wide, for instance, probabilistic programs are used in machine learning and robotics to describe distribution functions that are analyzed using Bayesian inference. In security, probabilistic programming has played a central role in cryptography, i.e., probabilistic security guarantees and probabilistic encryption. Probabilistic programs are also used to model the performance and reliability properties of a variety of systems, in which the uncertainties can come from the reliability of components (hardwares or softwares), the data from sensors, the reliability of the communication channels in the systems (e.g., the aircraft’s control systems).
This raises the question of how to analyze and verify that a system exhibiting probabilistic behavior satisfies a certain property. There is a rapidly growing trend in research on probabilistic programs which focuses on many aspects such as static analysis, program compilation, and program verification. To mention a few, the extension the framework of abstract interpretation to probabilistic programs, the development of a calculus for obtaining upper bounds on the expected value of run-time for probabilistic programs, and the developments of probabilistic and statistic model checking techniques for verifying probabilistic temporal properties of probabilistic and timed systems. In this work, we focus on answering the following question.
Can we automatically compute a symbolic plolynomial bound on the expected value of the resource consumption of a probabilistic program?
Note that a finite bound also ensures that the program terminates with finite number of evaluation steps, thus it terminates with probability 1.