Directed symbolic execution

dc.contributor.authorMa, Kin-Keung
dc.contributor.authorKhoo, Yit Phang
dc.contributor.authorFoster, Jeffrey S.
dc.contributor.authorHicks, Michael
dc.date.accessioned2011-04-19T18:17:33Z
dc.date.available2011-04-19T18:17:33Z
dc.date.issued2011-04-07
dc.description.abstractIn this paper, we study the problem of automatically finding program executions that reach a particular target line. This problem arises in many debugging scenarios, e.g., a developer might learn that a failure is possible on a particular line but might not know exactly how to reproduce the failure or even whether it is reproducible. This can happen particularly often for bug reports from static analysis tools, which can produce false positives. 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 Mix- CCBSE, a strategy in which CCBSE is composed with another search strategy to yield a hybrid that is more powerful than either strategy alone. We compare SDSE, CCBSE, and Mix-CCBSE with several existing strategies from the literature. We find that, while SDSE performs extremely well in many cases, it sometimes fails badly. However, by mixing CCBSE with KLEE's search strategy, we obtain a strategy that has the best overall performance across the strategies we studied.en_US
dc.identifier.urihttp://hdl.handle.net/1903/11374
dc.language.isoen_USen_US
dc.relation.ispartofseriesUM Computer Science Department;CS-TR-4979
dc.titleDirected symbolic executionen_US
dc.typeTechnical Reporten_US

Files

Original bundle
Now showing 1 - 1 of 1
Loading...
Thumbnail Image
Name:
CS-TR-4979-r1.pdf
Size:
370.6 KB
Format:
Adobe Portable Document Format
License bundle
Now showing 1 - 1 of 1
No Thumbnail Available
Name:
license.txt
Size:
1.8 KB
Format:
Item-specific license agreed upon to submission
Description: