Guiding dynamic symbolic execution toward unverified program executions

Maria Christakis, Peter Müller, Valentin Wüstholz

Abstract

Most techniques to detect program errors, such as testing, code reviews, and static program analysis, do not fully verify all possible executions of a program. They leave executions unverified when they do not check certain properties, fail to verify properties, or check properties under certain unsound assumptions such as the absence of arithmetic overflow.

BibTeX

@inproceedings{Christakis-al:ICSE16,
  author    = {Maria Christakis and
               Peter M{\"{u}}ller and
               Valentin W{\"{u}}stholz},
  title     = {Guiding dynamic symbolic execution toward unverified program executions},
  booktitle = {ICSE},
  pages     = {144--155},
  publisher = {{ACM}},
  year      = {2016},
}

Guiding dynamic symbolic execution toward unverified program executions

Abstract

Related papers