Skip to main content
Share Your Experience: Take the 2024 Developer Survey
6 votes
Accepted

Why backward symbolic execution is so unpopular?

Forward SE is easier to implement, composes better with other testing methods, and thus is more scalable. Usually, on industrial-scale workloads, it's not possible to enumerate all paths in the ...
D.W.'s user avatar
  • 12.1k
4 votes
Accepted

Practical approaches to solving whether programs will halt

Yes, an example of a system that performs this task is T2. It does not solve the halting problem but instead it only attempts to solve certain special cases. A overview is at https://en.wikipedia.org/...
Joshua Herman's user avatar
3 votes

Symbolic Execution is a case of Abstract Interpretation?

See Patrick Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes (Iterative methods for ...
Patrick Cousot's user avatar
2 votes

Computing the existence of a path in a code execution graph

As such, your problem seems to be NP-complete. To see the membership in NP, you can first guess a path, and then check that this path ends with $V_q$ and is valid. For the hardness part, we can ...
M.Monet's user avatar
  • 1,429

Only top scored, non community-wiki answers of a minimum length are eligible