Directed symbolic execution
1 Goal: reach particular target line (for debugging or for static analysis reports reproducing). 2 strategies:
- SDSE—shortest-distance symbolic execution uses a distance metric in an interprocedural CFG;
- CCBSE—call-chain-backward symbolic execution 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;
- Mix-CCBSE strategy (CCBSE + KLEE strategy).
Line reachability problem is equivalent to general problem to finding a particular program state.
Sergey Vartanov, 2007–2020