An experimental evaluation of a symbolic execution system

The author describes a symbolic execution system that assists in the construction of test data and the detection of program errors. The system automatically generates a subset of all possible execution paths in the program, according to a certain path selection criterion. It symbolically executes each one of these paths and creates conditions on input variables that cause the path to be executed. These conditions form a system of equalities and inequalities. Solving this system gives input variable values that cause the path to be executed. If the system of conditions for a path is insoluble, the path is infeasible. The author presents the results of experiments that have been carried out to evaluate the effectiveness of the system and the path selection criterion employed in it