Speculative Symbolic Execution

TL;DR

This paper introduces Speculative Symbolic Execution (SSE), a novel approach that reduces constraint solver invocations and speeds up symbolic execution for large programs by speculatively exploring branches.

Contribution

The paper proposes SSE, a new symbolic execution method that reduces solver calls and improves efficiency, along with an optimization technique implemented in SPF.

Findings

Reduces constraint solver invocations by 21-49%.

Speeds up symbolic execution by 23.6-43.6%.

Implemented and tested on six programs with positive results.

Abstract

Symbolic execution is an effective path oriented and constraint based program analysis technique. Recently, there is a significant development in the research and application of symbolic execution. However, symbolic execution still suffers from the scalability problem in practice, especially when applied to large-scale or very complex programs. In this paper, we propose a new fashion of symbolic execution, named Speculative Symbolic Execution (SSE), to speed up symbolic execution by reducing the invocation times of constraint solver. In SSE, when encountering a branch statement, the search procedure may speculatively explore the branch without regard to the feasibility. Constraint solver is invoked only when the speculated branches are accumulated to a specified number. In addition, we present a key optimization technique that enhances SSE greatly. We have implemented SSE and the optimization technique on Symbolic Pathfinder (SPF). Experimental results on six programs show that, our method can reduce the invocation times of constraint solver by 21% to 49% (with an average of 30%), and save the search time from 23.6% to 43.6% (with an average of 30%).