Symbolic Execution with Interval Solving and Meta-heuristic Search


A challenging problem in symbolic execution is to solve complex mathematical constraints such as constraints that include floating-point variables and transcendental functions. The inability to solve such constraints limit the application scope of symbolic execution. In this paper, we present a new method to solve such complex math constraints. Our method combines two existing: meta-heuristic search and interval solving. Conceptually, the combination explores the synergy of the individual methods to improve constraint solving. We implemented the new method in the CORAL constraint-solving infrastructure, and evaluated its effectiveness on a set of publicly-available software from the aerospace domain. Results indicate that the new method can solve significantly more complex mathematical constraints than previous techniques.

In IEEE International Conference on Software Testing, Verification and Validation (ICST).