See L. Kruglov letter, answer.

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.

Graphs

Sergey Vartanov, 2007–2020