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.
Denaro, G. (2012). All-Values Symbolic Execution. In Proceedings of the 7th International Workshop on Automation of Software Test (AST) (pp.138-144) [10.1109/IWAST.2012.6228982].
All-Values Symbolic Execution
DENARO, GIOVANNI
2012
Abstract
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.
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
