Reachability and symbolic execution

Question

Now I am confused about symbolic execution (SE) and reachability analysis (RA). As I know, SE uses symbols to execute some code to reach each branch with branch conditions. And RA can be used to find the reachability of each branch, right? When RA is used, we may extract the branch condition for each branch. If so, what's the difference between them? Can they be swift? Are they all static analysis?

Thanks, Eve

Answer 1

Symbolic execution is not static and it executes the program symbolically. For the concern of performance, symbolic execution tools like klee do not solve the branch condition when encountering a branch. It uses a cheap analysis to see whether it is likely to be reachable. It will try to generate a test case when reaching an exit of the program. If the collected constraints from the starting point (main function) to the exit is satisfiable, then a test case will be given, otherwise the exit is unreachable. SE uses reachability analysis to generate a test case to cover the code.

Answer 2

Symbolic execution is done without executing the program. It is therefore static analysis.

A good symbolic analysis will compute path conditions for each program point. A better one will be able to reason about the path formula, to demonstrate it is feasible (program point is reachable) or not (program point is dead).

Compared to execution rates of compiled code, symbolic execution tends to be pretty slow.

Answer 3

Reachability analysis is mostly used to see if a model can reach a state or not. However, Symbolic Execution is a static analysis technique (sometimes also dynamic, like what KLEE does) to find all the paths in a program/source code.