A segmented memory model for symbolic execution

Abstract

Symbolic execution is an effective technique for exploring paths in a program and reasoning about all possible values on those paths. However, the technique still struggles with code that uses complex heap data structures, in which a pointer is allowed to refer to more than one memory object. In such cases, symbolic execution typically forks execution into multiple states, one for each object to which the pointer could refer.

BibTeX

@inproceedings{Kapus-Cadar:FSE19,
  author    = {Timotej Kapus and
               Cristian Cadar},
  title     = {A segmented memory model for symbolic execution},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {774--784},
  publisher = {{ACM}},
  year      = {2019},
}

A segmented memory model for symbolic execution

Abstract

Related papers