Integrating assertion stack and caching to optimize constraint solving

Although significant advances have been made over the past few years, constraint solving is still the main bottleneck in symbolic execution. In fact, it often dominates the cost in overall performance. Thus, it is important to reduce the overhead in calling a constraint solver by exploring domain specific insights. In this paper, we propose a novel approach to optimize constraint solving. Our approach integrates two existing strategies: assertion stack and caching. We implemented a proof-of-concept tool based on Symbolic Pathfinder, a popular symbolic execution framework for JAVA programs. We have evaluated the tool on a set of open source software and the results showed that our approach can significantly improve the performance of constraint solving.