Exact and approximate probabilistic symbolic execution for nondeterministic programs
Abstract
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.
BibTeX
@inproceedings{Luckow-al:ASE14,
author = {Kasper S{\o}e Luckow and
Corina S. Pasareanu and
Matthew B. Dwyer and
Antonio Filieri and
Willem Visser},
title = {Exact and approximate probabilistic symbolic execution for nondeterministic programs},
booktitle = {ASE},
pages = {575--586},
publisher = {{ACM}},
year = {2014},
}