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?

  • 1
    $\begingroup$ Thanks for asking, Eve! What reading have you done to try to understand these topics? There is a lot written about them; you should start by reading some of the classic papers or descriptions in textbooks. If you tell us what you've read so far, we might be able to suggest further reading. Also, it might help to specify what you mean by reachability analysis; the term can mean different things, depending upon context and possibly upon the author/textbook. I suggest you edit your question to clarify these points. $\endgroup$
    – D.W.
    Jul 29, 2013 at 19:07

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.