Optimizing Constraint Solving to Better Support Symbolic Execution
Constraint solving is an integral part of symbolic execution, as most symbolic execution techniques rely heavily on an underlying constraint solver. In fact, the performance of the constraint solver used by a symbolic execution technique can considerably affect its overall performance. Unfortunately, constraint solvers are mostly used in a black-box fashion within symbolic execution, without leveraging any of the contextual and domain information available. Because constraint solvers are optimized for specific kinds of constraints and heavily based on heuristics, this leaves on the table many opportunities for optimizing the solvers' performance.