symbolic-execution

Is there a trade-off between pruning in symbolic execution and coverage as well as the final detection performance?


A common issue in symbolic execution is path explosion. Would using pruning and other heuristic strategies lead to decreased coverage and thus affect its effectiveness?


Solution

  • It depends on what you mean by "pruning."

    If you prune unreachable (dead) code, then no. If you prune reachable code, then yes it would. The trick is figuring out what's reachable and what isn't; which is the million dollar question in symbolic simulation. If you're entirely heuristic based, you'd have to be really "conservative" and only prune what you can determine is unreachable for sure to remain sound. But that problem itself can be as hard as the path explosion problem itself. (In a sense, it's exactly the same problem.)