Abstract: Symbolic execution is an effective and automatic bug-finding method. But symbolic execution is limited in practice by the computation cost and path explosion. We presented a tool for full-automatic detection and generating inputs that lead to memory safety violations in C programs, including buffer overflow, buffer overrun and pointer dereference error. In order to reduce the amount of symbol variable, we used the symbol variable to track the length of buffer and C string. The use of symbolic buffer length makes it possible to compactly summarize the behavior of standard buffer manipulation functions. While resolving the problem of path explosion, we introduced the dynamic slicing methods to prune the redundant paths. It's shown by the experiments that our method presented in this paper not only is feasible but also has little cost.

Key words: Static analysis, Symbolic execution, Program slicing, Constraint solving