Automated test generation on path-based symbolic execution

This paper describes the path-based symbolic execution of programs in order to solve the “path-storm” problem in traditional symbolic execution. Instead of using execution tree, execution digraph is used, and the program execution is simplified by clustering the execution of loops, and decrease the paths generated from the execution of loops by classifying the constraints. The verification and analysis of path-based symbolic execution algorithm are included.

I. Introduction

Symbolic execution is a natural extension of normal execution [1], which providing the normal computations as a special case. Many algorithms have been proposed in software automatic testing [2]–[3]. Computational definitions for the basic operators of the language are extended to accept symbolic inputs and produce symbolic formulas as output [4].