Loop Extended Symbolic Execution on List Manipulating Programs
Current symbolic execution is challenged by its ability to deal with loops. The case gets worse for loops manipulating recursive data structures. In this paper, we extend classic symbolic execution techniques for error detection of programs manipulating lists in loops. The idea is to enhance the symbolic execution with the utilization of quantitative aspect of the shape, and to construct the exit state of the loop. The exit state is constrained by a set of numeric constraints containing normal symbolic variables in programs and instrumented symbolic variables on the shapes. A prototype tool has been implemented and experiments are conducted on some commonly used list manipulating programs.
R. J. Li et al., "Loop Extended Symbolic Execution on List Manipulating Programs", Applied Mechanics and Materials, Vols. 130-134, pp. 3010-3014, 2012