Exact and approximate probabilistic symbolic execution for nondeterministic programs
Kasper Søe Luckow, Corina S. Păsăreanu, Matthew B. Dwyer, Antonio Filieri, Willem I. Visser · 2014
Probabilistic software analysis seeks to quantify the likelihood of reaching a target event under uncertain environments. Recent approaches compute probabilities of execution paths using symbolic execution, but do not support nondeterminism. Nondeterminism arises naturally when no suitable probabilistic model can capture a program behavior, e.g., for multithreading or distributed systems.