[1] Larochelle D, Evans D. Statically detecting likely buffer overflow vulnerabilities //Proceedings of 10th conference on USENIX Security Symposium. 2001.

[2] Godefroid P, Klarlund N, Sen K. DART: Directed automated random testing //ACM Sigplan Notices. 2005, 40: 213-223.

[3] Sen K, Agha G. CUTE and jCUTE: Concolic unit testing and explicit path model-checking tools //Proceedings of Conference on Computer Aided Verification. 2006, 4144: 419- 423.

[4] Cadar C, Ganesh V, Pawlowski P, et al. EXE: Automatically generating inputs of death
[J]. ACM Transactions on Information and System Security, 2008,12: 1-38.

[5] Horwitz S, Reps T. The use of program dependence graphs in software engineering //Proceedings of International Conference on Software Engineering. 1992: 392- 411.

[6] Van Engelen R. The CR# algebra and its application in loop analysis and optimization . Technical Report TR- 041223. Department of Computer Science, Florida State University, 2004.

[7] Van Engelen R, Birch J, Shou Y, et al. A unified framework for nonlinear dependence testing and symbolic analysis //Proceedings of the ACM International Conference on Supercomputing (ICS). 2004: 106-115.

[8] Cytron R, Ferrante J, Rosen B, et al. An efficient method of computing static single assignment form //Proceedings of 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 1989.

[9] Microsoft Research. Microsoft Phoenix Academic Program . . http://research.microsoft.com/phoenix/

[10] Microsoft Research. Z3: New High-performance Theorem Prover . . http://research.microsoft.com/projects/z3/

[11] Sourceforge. Cppcheck: A tool for static C/C+ + code analysis . . http://cppcheck.wiki.sourceforge.net/