On the probabilistic symbolic analysis of programs

Recently we have proposed symbolic execution techniques for the probabilistic analysis of programs. These techniques seek to quan- tify the probability of a program to satisfy a property of interest under a relevant usage profile. We describe recent advances in prob- abilistic symbolic analysis including handling of complex floating- point constraints and nondeterminism, and the use of statistical techniques for increased scalability