State of the art: Dynamic symbolic execution for automated test generation

Dynamic symbolic execution for automated test generation consists of instrumenting and running a program while collecting path constraint on inputs from predicates encountered in branch instructions, and of deriving new inputs from a previous path constraint by an SMT (Satisfiability Modulo Theories) solver in order to steer next executions toward new program paths. It has been introduced into several applications, such as automated test generation, automated filter generation and malware analysis mainly for its two intrinsic properties: low false positives and high code-coverage. In this paper, we focus on the topics that are closely related to automated test generation. Our contributions are five-fold. First, we summarize the theoretical foundation of dynamic symbolic execution. Second, we highlight the challenges when turning ideas into reality. Besides, we describe the state-of-the-art solutions including advantages and disadvantages for those challenges. In addition, twelve typical tools are analyzed and many properties of those tools are censused. Finally, we outline the prospects of this research field in detail.

► We summarize the theoretical foundation of dynamic symbolic execution.
► Several challenges of this research field are highlighted.
► We describe state-of-the-art solutions for those challenges.
► Twelve typical dynamic symbolic execution tools are analyzed and compared.
► We outline the prospects of this research field in detail.