SYMPAIS: SYMbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis

Probabilistic software analysis extends classic static analyses techniques to consider the effects of probabilistic uncertainty, whether explicitly embedded within the code - as in probabilistic program - or externalized in a probabilistic input distribution [Dwyer et al. 2016]. Similarly to their classic counterparts, these analyses aim at inferring the probability of a target event to occur during execution, e.g., reaching a program state or triggering an exception. For the probabilistic analysis of programs written in general-purpose programming languages, probabilistic symbolic execution (PSE) [Geldenhuys et al. 2012] exploits established symbolic execution engines for the language to extract constraints on probabilistic input or program variables that lead to the occurrence of the target event. The probability of satisfying any such constraints is then computed via model counting or inferred via solution space quantification methods, depending on the variable types and the characteristic of the constraints. Variations of PSE include incomplete analyses inferring probability bounds from a finite sample of program paths executed symbolically [Filieri et al. 2014], methods for non-deterministic programs [Luckow et al. 2014] and data structures [Filieri et al. 2015].