Probabilistic Programming: A True Verification Challenge

Probabilistic programs [6] are sequential programs, written in languages like C, Java, Scala, or ML, with two added constructs: (1) the ability to draw values at random from probability distributions, and (2) the ability to condition values of variables in a program through observations. For a comprehensive treatment, see [3]. They have a wide range of applications. Probabilistic programming is at the heart of machine learning for describing distribution functions; Bayesian inference is pivotal in their analysis. Probabilistic programs are central in security for describing cryptographic constructions (such as randomised encryption) and security experiments. In addition, probabilistic programs are an active research topic in quantitative information flow. Quantum programs are inherently probabilistic due to the random outcomes of quantum measurements. Finally, probabilistic programs can be used for approximate computing, e.g., by specifying reliability requirements for programs that allocate data in unreliable memory and use unreliable operations in hardware (so as to save energy dissipation) [1]. Other applications include [4] scientific modeling, information retrieval, bio–informatics, epidemiology, vision, seismic analysis, semantic web, business intelligence, human cognition, and more. Microsoft has started an initiative to improve the usability of probabilistic programming which has resulted in languages such as R2 [13] and Tabular [5] emerged.