{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,14]],"date-time":"2026-02-14T00:56:33Z","timestamp":1771030593415,"version":"3.50.1"},"reference-count":49,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2012,7,3]],"date-time":"2012-07-03T00:00:00Z","timestamp":1341273600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2012,12]]},"DOI":"10.1007\/s10515-012-0111-x","type":"journal-article","created":{"date-parts":[[2012,7,2]],"date-time":"2012-07-02T13:14:34Z","timestamp":1341234874000},"page":"531-559","source":"Crossref","is-referenced-by-count":30,"title":["StrSolve: solving string constraints lazily"],"prefix":"10.1007","volume":"19","author":[{"given":"Pieter","family":"Hooimeijer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Westley","family":"Weimer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2012,7,3]]},"reference":[{"key":"111_CR1","doi-asserted-by":"crossref","first-page":"410","DOI":"10.1007\/978-3-540-70583-3_34","volume-title":"International Colloquium on Automata, Languages and Programming","author":"R. Axelsson","year":"2008","unstructured":"Axelsson, R., Heljanko, K., Lange, M.: Analyzing context-free grammars using an incremental sat solver. In: International Colloquium on Automata, Languages and Programming, pp. 410\u2013422 (2008). doi: 10.1007\/978-3-540-70583-3_34"},{"key":"111_CR2","first-page":"387","volume-title":"IEEE Symposium on Security and Privacy","author":"D. Balzarotti","year":"2008","unstructured":"Balzarotti, D., Cova, M., Felmetsger, V., Jovanovic, N., Kirda, E., Kruegel, C., Vigna, G.: Saner: composing static and dynamic analysis to validate sanitization in web applications. In: IEEE Symposium on Security and Privacy, pp. 387\u2013401 (2008)"},{"key":"111_CR3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"N. Bj\u00f8rner","year":"2009","unstructured":"Bj\u00f8rner, N., Tillmann, N., Voronkov, A.: Path feasibility analysis for string-manipulating programs. In: Tools and Algorithms for the Construction and Analysis of Systems (2009)"},{"issue":"8","key":"111_CR4","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"35","author":"R.E. Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. 35(8), 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"key":"111_CR5","first-page":"1066","volume-title":"International Conference on Software Engineering","author":"C. Cadar","year":"2011","unstructured":"Cadar, C., Godefroid, P., Khurshid, S., Pasareanu, C.S., Sen, K., Tillmann, N., Visser, W.: Symbolic execution for software testing in practice: preliminary assessment. In: International Conference on Software Engineering, pp. 1066\u20131071 (2011)"},{"key":"111_CR6","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"International Symposium on Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: International Symposium on Static Analysis, pp. 1\u201318 (2003)"},{"key":"111_CR7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L.M. Moura de","year":"2008","unstructured":"de Moura, L.M., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems (2008)"},{"issue":"3","key":"111_CR8","doi-asserted-by":"crossref","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365\u2013473 (2005). doi: 10.1145\/1066100.1066102","journal-title":"J. ACM"},{"key":"111_CR9","first-page":"502","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2003","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Theory and Applications of Satisfiability Testing, pp. 502\u2013518 (2003)"},{"key":"111_CR10","first-page":"67","volume-title":"Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215","author":"X. Fu","year":"2010","unstructured":"Fu, X., Li, C.C.: Modeling regular replacement for string constraint solving. In: Mu\u00f1oz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215, NASA, Langley Research Center, Hampton, VA 23681-2199, USA, pp. 67\u201376 (2010)"},{"key":"111_CR11","doi-asserted-by":"crossref","unstructured":"Fu, X., Powell, M., Bantegui, M., Li, C.C.: Simple linear string constraints. Form. Asp. Comput. 1\u201345 (2012). doi: 10.1007\/s00165-011-0214-3","DOI":"10.1007\/s00165-011-0214-3"},{"key":"111_CR12","unstructured":"Fujitsu Laboratories: Fujitsu develops technology to enhance comprehensive testing of Java programs (2010). URL http:\/\/www.fujitsu.com\/global\/news\/pr\/archives\/month\/2010\/20100112-02.html"},{"key":"111_CR13","doi-asserted-by":"crossref","first-page":"519","DOI":"10.1007\/978-3-540-73368-3_52","volume-title":"Computer-Aided Verification","author":"V. Ganesh","year":"2007","unstructured":"Ganesh, V., Dill, D.L.: A decision procedure for bit-vectors and arrays. In: Computer-Aided Verification, pp. 519\u2013531 (2007)"},{"key":"111_CR14","volume-title":"Programming Language Design and Implementation","author":"P. Godefroid","year":"2005","unstructured":"Godefroid, P., Klarlund, N., Sen, K.: DART: directed automated random testing. In: Programming Language Design and Implementation (2005)"},{"key":"111_CR15","volume-title":"Programming Language Design and Implementation","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Kiezun, A., Levin, M.Y.: Grammar-based whitebox fuzzing. In: Programming Language Design and Implementation (2008a)"},{"key":"111_CR16","volume-title":"Network Distributed Security Symposium","author":"P. Godefroid","year":"2008","unstructured":"Godefroid, P., Levin, M., Molnar, D.: Automated whitebox fuzz testing. In: Network Distributed Security Symposium (2008b)"},{"key":"111_CR17","series-title":"LNCS","volume-title":"TACAS \u201995","author":"J. Henriksen","year":"1995","unstructured":"Henriksen, J., Jensen, J., J\u00f8rgensen, M., Klarlund, N., Paige, B., Rauhe, T., Sandholm, A.: Mona: monadic second-order logic in practice. In: TACAS \u201995. LNCS, vol. 1019. Springer, Berlin (1995)"},{"key":"111_CR18","doi-asserted-by":"crossref","first-page":"248","DOI":"10.1007\/978-3-642-18275-4_18","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"P. Hooimeijer","year":"2011","unstructured":"Hooimeijer, P., Veanes, M.: An evaluation of automata algorithms for string analysis. In: Verification, Model Checking, and Abstract Interpretation, pp. 248\u2013262 (2011)"},{"key":"111_CR19","first-page":"188","volume-title":"Programming Languages Design and Implementation","author":"P. Hooimeijer","year":"2009","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Programming Languages Design and Implementation, pp. 188\u2013198 (2009)"},{"key":"111_CR20","first-page":"377","volume-title":"Automated Software Engineering","author":"P. Hooimeijer","year":"2010","unstructured":"Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Automated Software Engineering, pp. 377\u2013386 (2010)"},{"key":"111_CR21","first-page":"1","volume-title":"USENIX Security Symposium","author":"P. Hooimeijer","year":"2011","unstructured":"Hooimeijer, P., Livshits, B., Molnar, D., Saxena, P., Veanes, M.: Fast and precise sanitizer analysis with bek. In: USENIX Security Symposium, pp. 1\u201315 (2011)"},{"issue":"1","key":"111_CR22","doi-asserted-by":"crossref","first-page":"140","DOI":"10.1016\/S0890-5401(03)00090-7","volume":"186","author":"L. Ilie","year":"2003","unstructured":"Ilie, L., Yu, S.: Follow automata. Inf. Comput. 186(1), 140\u2013162 (2003). doi: 10.1016\/S0890-5401(03)00090-7","journal-title":"Inf. Comput."},{"key":"111_CR23","first-page":"105","volume-title":"International Symposium on Software Testing and Analysis","author":"A. Kiezun","year":"2009","unstructured":"Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: Hampi: a solver for string constraints. In: International Symposium on Software Testing and Analysis, pp. 105\u2013116 (2009)"},{"key":"111_CR24","first-page":"1759","volume-title":"Proceedings of the Genetic and Evolutionary Computation Conference","author":"K. Lakhotia","year":"2008","unstructured":"Lakhotia, K., McMinn, P., Harman, M.: Handling dynamic data structures in search based testing. In: Proceedings of the Genetic and Evolutionary Computation Conference, pp. 1759\u20131766 (2008)"},{"key":"111_CR25","doi-asserted-by":"crossref","first-page":"95","DOI":"10.1109\/TAICPART.2009.15","volume-title":"Testing Academia and Industry Conference","author":"K. Lakhotia","year":"2009","unstructured":"Lakhotia, K., McMinn, P., Harman, M.: Automated test data generation for coverage: haven\u2019t we solved this problem yet? In: Testing Academia and Industry Conference, pp. 95\u2013104 (2009)"},{"issue":"12","key":"111_CR26","doi-asserted-by":"crossref","first-page":"2379","DOI":"10.1016\/j.jss.2010.07.026","volume":"83","author":"K. Lakhotia","year":"2010","unstructured":"Lakhotia, K., McMinn, P., Harman, M.: An empirical investigation into branch coverage for c programs using cute and Austin. J. Syst. Softw. 83(12), 2379\u20132391 (2010)","journal-title":"J. Syst. Softw."},{"key":"111_CR27","volume-title":"Automated Software Engineering Short Paper","author":"N. Li","year":"2009","unstructured":"Li, N., Xie, T., Tillmann, N., de Halleux, J., Schulte, W.: Reggae: automated test generation for programs using complex regular expressions. In: Automated Software Engineering Short Paper (2009)"},{"key":"111_CR28","first-page":"416","volume-title":"International Conference on Software Engineering","author":"R. Majumdar","year":"2007","unstructured":"Majumdar, R., Sen, K.: Hybrid concolic testing. In: International Conference on Software Engineering, pp. 416\u2013426 (2007)"},{"key":"111_CR29","first-page":"134","volume-title":"Automated Software Engineering","author":"R. Majumdar","year":"2007","unstructured":"Majumdar, R., Xu, R.G.: Directed test generation using symbolic grammars. In: Automated Software Engineering, pp. 134\u2013143 (2007)"},{"key":"111_CR30","doi-asserted-by":"crossref","first-page":"432","DOI":"10.1145\/1060745.1060809","volume-title":"International Conference on the World Wide Web","author":"Y. Minamide","year":"2005","unstructured":"Minamide, Y.: Static approximation of dynamically generated web pages. In: International Conference on the World Wide Web, pp. 432\u2013441 (2005). http:\/\/doi.acm.org\/10.1145\/1060745.1060809"},{"key":"111_CR31","first-page":"221","volume-title":"Programming Language Design and Implementation","author":"A. M\u00f8ller","year":"2001","unstructured":"M\u00f8ller, A., Schwartzbach, M.I.: The pointer assertion logic engine. In: Programming Language Design and Implementation, pp. 221\u2013231 (2001)"},{"key":"111_CR32","first-page":"530","volume-title":"Design Automation Conference","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Design Automation Conference, pp. 530\u2013535 (2001)"},{"key":"111_CR33","first-page":"106","volume-title":"Principles of Programming Languages","author":"G.C. Necula","year":"1997","unstructured":"Necula, G.C.: Proof-carrying code. In: Principles of Programming Languages, pp. 106\u2013119 (1997)"},{"key":"111_CR34","first-page":"15","volume-title":"International Symposium on Software Testing and Analysis","author":"C.S. Pasareanu","year":"2008","unstructured":"Pasareanu, C.S., Mehlitz, P.C., Bushnell, D.H., Gundy-Burlet, K., Lowry, M.R., Person, S., Pape, M.: Combining unit-level symbolic execution and system-level concrete execution for testing NASA software. In: International Symposium on Software Testing and Analysis, pp. 15\u201326 (2008)"},{"key":"111_CR35","doi-asserted-by":"crossref","first-page":"513","DOI":"10.1109\/SP.2010.38","volume-title":"IEEE Symposium on Security and Privacy","author":"P. Saxena","year":"2010","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. In: IEEE Symposium on Security and Privacy, pp. 513\u2013528 (2010)"},{"key":"111_CR36","volume-title":"Introduction to the Theory of Computation","author":"M. Sipser","year":"1997","unstructured":"Sipser, M.: Introduction to the Theory of Computation, 2nd edn. Course Technology, Independence (1997)","edition":"2"},{"key":"111_CR37","first-page":"372","volume-title":"Principles of Programming Languages","author":"Z. Su","year":"2006","unstructured":"Su, Z., Wassermann, G.: The essence of command injection attacks in web applications. In: Principles of Programming Languages, pp. 372\u2013382 (2006)"},{"key":"111_CR38","first-page":"166","volume-title":"ISSTA \u201911","author":"T. Tateishi","year":"2011","unstructured":"Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. In: ISSTA \u201911, pp. 166\u2013176. ACM, New York (2011)"},{"key":"111_CR39","doi-asserted-by":"crossref","first-page":"498","DOI":"10.1109\/ICST.2010.15","volume-title":"International Conference on Software Testing, Verification and Validation","author":"M. Veanes","year":"2010","unstructured":"Veanes, M., de Halleux, P., Tillmann, N.: Rex: symbolic regular expression explorer. In: International Conference on Software Testing, Verification and Validation, pp. 498\u2013507 (2010)"},{"key":"111_CR40","first-page":"137","volume-title":"Principles of Programming Languages","author":"M. Veanes","year":"2012","unstructured":"Veanes, M., Hooimeijer, P., Livshits, B., Molnar, D., Bj\u00f8rner, N.: Symbolic finite state transducers: algorithms and applications. In: Principles of Programming Languages, pp. 137\u2013150 (2012)"},{"key":"111_CR41","first-page":"32","volume-title":"Programming Languages Design and Implementation","author":"G. Wassermann","year":"2007","unstructured":"Wassermann, G., Su, Z.: Sound and precise analysis of web applications for injection vulnerabilities. In: Programming Languages Design and Implementation, pp.\u00a032\u201341 (2007)"},{"key":"111_CR42","volume-title":"International Conference on Software Engineering","author":"G. Wassermann","year":"2008","unstructured":"Wassermann, G., Su, Z.: Static detection of cross-site scripting vulnerabilities. In: International Conference on Software Engineering (2008)"},{"key":"111_CR43","first-page":"364","volume-title":"International Conference on Software Engineering","author":"W. Weimer","year":"2009","unstructured":"Weimer, W., Nguyen, T., Le Goues, C., Forrest, S.: Automatically finding patches using genetic programming. In: International Conference on Software Engineering, pp. 364\u2013374 (2009)"},{"key":"111_CR44","doi-asserted-by":"crossref","first-page":"139","DOI":"10.1007\/11513988_13","volume-title":"Computer Aided Verification","author":"Y. Xie","year":"2005","unstructured":"Xie, Y., Aiken, A.: Saturn: a SAT-based tool for bug detection. In: Computer Aided Verification, pp. 139\u2013143 (2005)"},{"key":"111_CR45","first-page":"179","volume-title":"USENIX Security Symposium","author":"Y. Xie","year":"2006","unstructured":"Xie, Y., Aiken, A.: Static detection of security vulnerabilities in scripting languages. In: USENIX Security Symposium, pp. 179\u2013192 (2006)"},{"key":"111_CR46","first-page":"605","volume-title":"Automated Software Engineering","author":"F. Yu","year":"2009","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Generating vulnerability signatures for string manipulating programs using automata-based forward and backward symbolic analyses. In: Automated Software Engineering, pp. 605\u2013609 (2009a)"},{"key":"111_CR47","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Yu","year":"2009","unstructured":"Yu, F., Bultan, T., Ibarra, O.H.: Symbolic string verification: combining string analysis and size analysis. In: Tools and Algorithms for the Construction and Analysis of Systems (2009b)"},{"key":"111_CR48","first-page":"290","volume-title":"Conference on Implementation and Application of Automata","author":"F. Yu","year":"2010","unstructured":"Yu, F., Bultan, T., Ibarra, O.H.: Relational string verification using multi-track automata. In: Conference on Implementation and Application of Automata, pp. 290\u2013299 (2010)"},{"key":"111_CR49","first-page":"251","volume-title":"International Conference on Software Engineering","author":"F. Yu","year":"2011","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Patching vulnerabilities with sanitization synthesis. In: International Conference on Software Engineering, pp. 251\u2013260 (2011)"}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0111-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-012-0111-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-012-0111-x","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,1,20]],"date-time":"2022-01-20T01:27:08Z","timestamp":1642642028000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-012-0111-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,7,3]]},"references-count":49,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["111"],"URL":"https:\/\/doi.org\/10.1007\/s10515-012-0111-x","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,7,3]]}}}