[1] Zhang D L, Sui J W, Gong Y Z. Large scale software test data generation based on collective constraint and weighted combination method. Tehni?ki Vjesnik, 2017, 24(4):10411049.
[2] Zhang Z X, Chen Z Y, Gao R Z, Wong E W, Xu B W. An empirical study on constraint optimization techniques for test generation. Science China Information Sciences, 2017, 60(1):012105
[3] Bjørner N, Tillmann N, Voronkov A. Path feasibility analysis for stringmanipulating programs. In Tools and Algorithms for the Construction and Analysis of Systems, Kowalewski S, Philippou A (eds.), Springer, 2009, pp.307321.
[4] Hooimeijer P, Weimer W. A decision procedure for subset constraints over regular languages. ACM SIGPLAN Notices, 2009, 44(6):188198.
[5] Tillmann N, de Halleux J. Pexwhite box test generation for.NET. In Tests and Proofs, Beckert B, Hähnle R (eds.), Springer, 2008, pp.134153.
[6] Wang Y W, Xing Y, Gong Y Z, Zhang X Z. Optimized branch and bound for pathwise test data generation. Int. Journal of Computers Communications & Control, 2014, 9(4):497509.
[7] Liang T Y, Reynolds A, Tinelli C, Barrett C, Deters M. A DPLL(T) theory solver for a theory of strings and regular expressions. In Computer Aided Verification, Biere A, Bloem R (eds.), Springer, 2014, pp.646662.
[8] van Benthem J, Doets K. Higherorder logic. In Handbook of Philosophical Logic, Gabbay D, Guenthner F (eds.), Springer, 1983, pp.275329
[9] Khoussainov B, Nies A, Rubin S, Stephan F. Automatic structures:Richness and limitations. In Proc. the 19th Annual IEEE Symp. Logic in Computer Science, July 2004, pp.4453.
[10] Nieuwenhuis R, Oliveras A, Tinelli C. Solving SAT and SAT modulo theories:From an abstract DavisPutnamLogemannLoveland procedure to DPLL(T). Journal of the ACM, 2006, 53(6):937977.
[11] Kiezun A, Ganesh V, Guo P J, Hooimeijer P, Ernst M D. HAMPI:A solver for string constraints. In Proc. the 18th Int. Symp. Software Testing and Analysis, July 2009, pp.105116.
[12] Ganesh V, Dill D L. A decision procedure for bitvectors and arrays. In Computer Aided Verification, Damm W, Hermanns H (eds.), Springer, 2007, pp.519531.
[13] Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D. A symbolic execution framework for JavaScript. In Proc. IEEE Symp. Security and Privacy, May 2010, pp.513528.
[14] de Moura L, Bjørner N. Z3:An efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, Ramakrishnan C R, Rehof J (eds.), Springer, 2008, pp.337340.
[15] Zheng Y H, Zhang X Y, Ganesh V. Z3str:A Z3based string solver for web application analysis. In Proc. the 9th Joint Meeting on Foundations of Software Engineering, August 2013, pp.114124.
[16] Trinh M T, Chu D H, Jaffar J. S3:A symbolic string solver for vulnerability detection in web applications. In Proc. ACM SIGSAC Conf. Computer and Communications Security, November 2014, pp.12321243.
[17] Stump A, Barrett C W, Dill D L. CVC:A cooperating validity checker. In Computer Aided Verification, Brinksma E, Larsen K G (eds.), Springer, 2002, pp.500504.
[18] Hooimeijer P, Weimer W. Solving string constraints lazily. In Proc. IEEE/ACM Int. Conf. Automated Software Engineering, September 2010, pp.377386.
[19] Veanes M, de Halleux P, Tillmann N. Rex:Symbolic regular expression explorer. In Proc. the 3rd Int. Conf. Software Testing, Verification and Validation, April 2010, pp.498507.
[20] Ghosh I, Shafiei N, Li G D, Chiang W F. JST:An automatic test generation tool for industrial Java applications with strings. In Proc. the 35th Int. Conf. Software Engineering, May 2013, pp.9921001.
