Statistical symbolic execution with informed sampling

Abstract

Probabilistic program analysis aims at quantifying the probability of a target event to occur during a program execution. Recent approaches exploit symbolic execution to compute the constraints on the inputs leading to the occurrence of a target event; the solution space for such constraints is then quantified given a probabilistic usage profile, which characterizes each input variable by a probability distribution over its possible values. Despite their generality and accuracy, these exhaustive approaches suffer scalability issues for large programs.