A hybrid path constraint solver combined with meta-heuristic search

ABSTRACT. Constraint solving is one of the essential parts of symbolic execution. Most of the constraint solvers are aimed at a particular kind of constraint and might have no way to deal with complex path constraints derived from real-world applications. To tackle the problem, we propose a hybrid solving strategy for path constraints containing multiple kinds of constraints. In particular, a split approach is used to cut the whole path constraint into several parts that can be solved by different constraint solving techniques. Next, the local method of meta-heuristic search is used to solve non-linear constraints led by the solutions produced by a linear constraint solver. We have extended the constraint solver in the symbolic execution engine KLEE-FP with our approach and evaluated its effectiveness on a set of mathematical programs. The results show that our approach can solve a majority of complex path constraints in reasonable time.