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 ...
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/...
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 ...
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 ...
What is the state of the art in cache algorithm theory?
I don't know about a method for analyzing an arbitrary given algorithm to come up with a cache policy in general (this sounds quite hard), but this is essentially what's been done (optimally, in an ...
Only top scored, non community-wiki answers of a minimum length are eligible