2
$\begingroup$

Looking at the Symbolic Execution limitations, there are some good solutions to the "Environment interactions" problems. However, the solutions to the path explosion problem are less than ideal.

Solutions to the path explosion problem generally use either heuristics for path-finding to increase code coverage,[2] reduce execution time by parallelizing independent paths,[3] or by merging similar paths.[4]

The parallelizing is just adding more power to the situation which doesn't really solve it. The first and third suggestions I am not to familiar with. The first sounds like it has similar problems to testing, in that they are just opting into certain paths based on heuristics, which also doesn't seem to solve it. I am wondering if the solutions to the path explosion problem could be explained here a little bit, either the solutions listed above or anything else. Specifically I am interested in the heuristics one, and what kind of things can be done here.

enter image description here

Improve this question
$\endgroup$
1
  • 1
    $\begingroup$ They helpfully give you a reference where you can read more to learn more about those methods. Have you read those references? This site works best when you study existing resources yourself before asking here. $\endgroup$
    – D.W. ♦
    Commented Jul 10, 2018 at 17:19

2 Answers 2

Reset to default
3
$\begingroup$

The heuristic approach to solving the path explosion problem picks the next branch to explore based on some function. A simple heuristic function, yet pretty effective, would be to assign the score of a branch based on how many times it has been seen before, and then pick the one with the lowest score. This ensures that branches which haven't been seen yet are explored first instead of getting stuck in a path explosion, whose branches would have been seen many times.

Improve this answer
$\endgroup$
2
$\begingroup$

There are two major things that cause path explosion: loops and large programs.

There is one clever solution to loops in this paper, Efficient Loop Navigation for Symbolic Execution. I don't fully understand it yet, but it transforms complicated nested loops into nested chains from which it creates a full sub-constraint system to solve within the context of the higher-level symbolic evaluator. They describe it in detail.

Also note that "dynamic symbolic execution" combines concrete execution with symbolic execution. Some approaches using dynamic symbolic evaluation interleave concrete inputs occasionally to test for values and perform other heuristics to guide navigation.

In terms of large programs, the problem is that you can have very large path conditions based on a very large number of possible ways to get to a specific state. This is similar in some ways to the problem of looping. The solution to this is to use compositional symbolic execution. This provides a summary for the input/output behavior of a function. So if the program is a bunch of functions composed together, you can eliminate the need to invoke each function again and again by summarizing its input/output behavior. This abstracts away the problem of having large path conditions and large numbers of paths related to complicated ways of getting to the state through the source code.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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