Efficient Loop Navigation for Symbolic Execution

Understand

Symbolic execution is a successful and very popular technique used in software verification and testing.

• A key limitation of symbolic execution is in dealing with code containing loops.
• The problem is that even a single loop can generate a huge number of different symbolic execution paths, corresponding to different number of loop iterations and taking various paths through the loop.
• We introduce a technique which, given a start location above some loops and a target location anywhere below these loops, returns a feasible path between these two locations, if such a path exists.