Symbolic Parallel Adaptive Importance Sampling for Probabilistic Program Analysis
This addresses scalability issues in probabilistic software analysis for mission-critical systems, offering a more general solution, though it appears incremental as it builds on existing techniques like importance sampling and symbolic execution.
The paper tackles the problem of analyzing probabilistic programs with high-dimensional, correlated input distributions, which existing methods struggle to scale with, by introducing SYMPAIS, a method that combines importance sampling and constraint solving to accurately estimate rare event probabilities, demonstrating improved performance over state-of-the-art alternatives across various domains.
Probabilistic software analysis aims at quantifying the probability of a target event occurring during the execution of a program processing uncertain incoming data or written itself using probabilistic programming constructs. Recent techniques combine symbolic execution with model counting or solution space quantification methods to obtain accurate estimates of the occurrence probability of rare target events, such as failures in a mission-critical system. However, they face several scalability and applicability limitations when analyzing software processing with high-dimensional and correlated multivariate input distributions. In this paper, we present SYMbolic Parallel Adaptive Importance Sampling (SYMPAIS), a new inference method tailored to analyze path conditions generated from the symbolic execution of programs with high-dimensional, correlated input distributions. SYMPAIS combines results from importance sampling and constraint solving to produce accurate estimates of the satisfaction probability for a broad class of constraints that cannot be analyzed by current solution space quantification methods. We demonstrate SYMPAIS's generality and performance compared with state-of-the-art alternatives on a set of problems from different application domains.