Test ranges (from siddiqui:oopsla:2012) compactly represent sets of program paths. using a pair of paths to define a range of paths based on lexicographic ordering of the paths and can be used to divide the symbolic execution tree into a number of subtrees that can be explored in parallel.
This paper adds feasible ranges and unexplored ranges
Feasible ranges start with a shallow exploration of the tree up to a small depth detecting infeasible branches as it goes and then splits the tree into subtrees that only contain feasible paths. This shares constraint solving results without sharing large constraint databases.
Unexplored ranges start with the results of some other test generation tool and identifies unexplored ranges for SE to explore.
Implemented using work-stealing, in Symbolic PathFinder
Notes related to A synergistic approach for distributed symbolic execution using test ranges
Swarm verification, Verifier performance
Papers related to A synergistic approach for distributed symbolic execution using test ranges
- Using test ranges to improve symbolic execution [qiu:nfm:2018]
- Scaling symbolic execution using ranged analysis [siddiqui:oopsla:2012]