Directed Symbolic Execution. Kin-Keung Ma, Yit Phang Khoo, Jeffrey S. Foster, and Michael Hicks. In Eran Yahav, editor, Proceedings of the Static Analysis Symposium (SAS), volume 6887 of Lecture Notes in Computer Science, pages 95--111. Springer, September 2011.

In this paper, we study the problem of automatically finding program executions that reach a particular target line. This problem arises in many debugging scenarios; for example, a developer may want to confirm that a bug reported by a static analysis tool on a particular line is a true positive. We propose two new directed symbolic execution strategies that aim to solve this problem: shortest-distance symbolic execution (SDSE) uses a distance metric in an interprocedural control flow graph to guide symbolic execution toward a particular target; and call-chain-backward symbolic execution (CCBSE) iteratively runs forward symbolic execution, starting in the function containing the target line, and then jumping backward up the call chain until it finds a feasible path from the start of the program. We also propose a hybrid strategy, Mix-CCBSE, which alternates CCBSE with another (forward) search strategy. We compare these three with several existing strategies from the literature on a suite of six GNU coreutils programs. We find that SDSE performs extremely well in many cases but may fail badly. CCBSE also performs quite well, but imposes additional overhead that sometimes makes it slower than SDSE. Considering all our benchmarks together, Mix-CCBSE performed best on average, combining to good effect the features of its constituent components.

.pdf ]

@inproceedings{ma11directed,
  title = {Directed Symbolic Execution},
  author = {Kin-Keung Ma and Yit Phang Khoo and Jeffrey S. Foster and Michael Hicks},
  booktitle = {Proceedings of the Static Analysis Symposium (SAS)},
  series = {Lecture Notes in Computer Science},
  volume = {6887},
  editor = {Eran Yahav},
  publisher = {Springer},
  pages = {95--111},
  year = 2011,
  month = sep
}

This file was generated by bibtex2html 1.99.