Lazy-substitution based symbolic execution for C programs

Lazy-substitution based symbolic execution was presented in order to address the computed memory location problem in traditional symbolic execution. A form of lazy strategy was introduced into traditional symbolic execution, which substitutes program variables with their symbolic values as much as possible. When the memory locations of variables in a statement can't be determined statically or the length of a symbolic expression for substitution is too long, those variables won't be replaced with their symbolic values. The lazy substitution algorithm was provided. Moreover, the lazy symbolic execution semantics for most of structures in C programming language were discussed in detail, especially for array and pointer. The prototype of symbolic execution system LazySEC (a lazy symbolic executor for C programs) performs lazy-substitution based symbolic execution for C programs. Preliminary experiment results show that LazySEC can handle program structures involving computed memory locations efficiently.