All-values symbolic execution

This paper discusses and exemplifies our ideas on all-values symbolic execution, an alternative strategy to the traditional all-paths style of symbolic execution. All-values symbolic execution focuses on enumerating the (symbolic) values that may derive from the symbolic execution of program statements. It exploits program dependencies to optimize the symbolic execution of those statements that can be executed with the same symbolic inputs on multiple (up to infinite) paths. Although a fully working implementation and a thorough evaluation are yet to come, this paper illustrates with simple, but representative examples that the proposed technique can boost the efficiency of symbolic execution, and suite interesting new applications.