Enhancing constraint based test generation by local search

The core operation of symbolic execution based test data generation is to generate a path constraint in terms of input variables for a selected path. Solutions to the path constraint are test data which will be used to execute the target path. So far, the limitations of constraint solving still prevent its widespread use in practice. Most of the constraint solvers aim at a particular kind of constraint and might have no way to deal with complex path constraints derived in a real-world software application. To tackle the problem, we propose a hybrid solving strategy for path constraints containing multiple kinds of constraints. In particular, the path constraint is converted and divided into two parts that can be solved by different constraint solving techniques. A local search method is combined with a linear constraint solver to solve complex mathematical constraints. We have extended the symbolic execution engine KLEE with our approach and evaluated its effectiveness on a set of mathematical programs. The preliminary evaluation shows that our approach can solve a majority of complex path constraints in the experiments in reasonable time.