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 classic static analysis methods with inference
procedure to obtain accurate quantification of the probability of rare target
events, such as failures in a mission-critical system. However, current
techniques face several scalability and applicability limitations when
analyzing software processing with high-dimensional multivariate distributions.
In this paper, we present SYMbolic Parallel Adaptive Importance Sampling
(SYMPAIS), a new algorithm that combines symbolic execution with adaptive
importance sampling to analyze probabilistic programs. Our method provides a
general solution that scales to systems with high-dimensional inputs and
demonstrates superior performance in quantifying rare events compared to prior
work. Preliminary experimental results support the potential efficacy of our
solution.