symMMU: symbolically executed runtime libraries for symbolic memory access

Abstract

Symbolic execution calls for specialized address translation. Unlike a pointer on a traditional machine model, which corresponds to a single address, a symbolic pointer may represent multiple feasible addresses. A symbolic pointer dereference manipulates symbolic state, potentially submitting many theorem prover requests in the process. Hence, design and management of symbolic accesses critically affects symbolic executor performance, complexity, and completeness.

BibTeX

@inproceedings{Romano-Engler:ASE14,
  author    = {Anthony Romano and
               Dawson R. Engler},
  title     = {{symMMU:} symbolically executed runtime libraries for symbolic memory access},
  booktitle = {ASE},
  pages     = {247--258},
  publisher = {{ACM}},
  year      = {2014},
}

symMMU: symbolically executed runtime libraries for symbolic memory access

Abstract

Related papers