Q:

Difference between symbolic execution and reachability analysis

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 can extract the branch condition for each branch. If so, what's the difference between them? Can they be swift? Are they all static analysis?

A:

Generally, reachability analysis is a goal (determine which points in the code are reachable), whereas symbolic execution is a specific algorithmic technique (a tool for analyzing code).  You can use symbolic execution for reachability analysis, or for other goals.  Conversely, you can use other algorithms for reachability analysis.
Classically, symbolic execution was a static analysis.  However, recently it has been widely used in a hybrid static-dynamic analysis: see, e.g., concolic execution.  These hybrid methods seem to be very effective, but they are not purely static.

