Context-sensitive relevancy analysis for efficient symbolic execution

Abstract. Symbolic execution is a flexible and powerful, but computa-tionally expensive technique to detect dynamic behaviors of a program. In this paper, we present a context-sensitive relevancy analysis algorithm based on weighted pushdown model checking, which pinpoints memory locations in the program where symbolic values can flow into. This in-formation is then utilized by a code instrumenter to transform only rele-vant parts of the program with symbolic constructs, to help improve the efficiency of symbolic execution of Java programs. Our technique is eval-uated on a generalized symbolic execution engine that is developed upon Java Path Finder with checking safety properties of Java applications. Our experiments indicate that this technique can effectively improve the performance of the symbolic execution engine with respect to the ap-proach that blindly instruments the whole program.