Type-Dependence Analysis and Program Transformation for Symbolic Execution

Symbolic execution can be problematic when applied to real applications. This paper addresses two of these problems: (1) the constraints generated during symbolic execution may be of a type not handled by the underlying decision procedure, and (2) some parts of the application may be unsuitable for symbolic execution (e.g., third-party libraries). The paper presents type-dependence analysis, which performs a context- and field-sensitive interprocedural static analysis to identify program entities that may store symbolic values at run-time. This information is used to identify the above two problematic cases and assist the user in addressing them. The paper also presents a technique to transform real applications for efficient symbolic execution. Instead of transforming the entire application, which can be inefficient and infeasible (mostly for pragmatic reasons), our technique leverages the results of type-dependence analysis to transform only parts of the program that may interact wi...

• Type: Conference
• Year: 2007
• Where: TACAS
• Authors: Saswat Anand, Alessandro Orso, Mary Jean Harrold
• Keywords: Algorithms, Real Applications, Symbolic Execution, Symbolic Values, TACAS 2007