{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,5]],"date-time":"2026-03-05T17:56:51Z","timestamp":1772733411892,"version":"3.50.1"},"reference-count":41,"publisher":"Springer Science and Business Media LLC","issue":"2-3","license":[{"start":{"date-parts":[[2016,12,27]],"date-time":"2016-12-27T00:00:00Z","timestamp":1482796800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2017,6]]},"DOI":"10.1007\/s10703-016-0263-6","type":"journal-article","created":{"date-parts":[[2016,12,27]],"date-time":"2016-12-27T06:12:04Z","timestamp":1482819124000},"page":"249-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Z3str2: an efficient solver for strings, regular expressions, and length constraints"],"prefix":"10.1007","volume":"50","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6794-3199","authenticated-orcid":false,"given":"Yunhui","family":"Zheng","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vijay","family":"Ganesh","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sanu","family":"Subramanian","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Omer","family":"Tripp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Murphy","family":"Berzish","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julian","family":"Dolby","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Xiangyu","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,12,27]]},"reference":[{"key":"263_CR1","unstructured":"Z3str2 String Constraint Solver. https:\/\/sites.google.com\/site\/z3strsolver\/"},{"key":"263_CR2","unstructured":"IBM Security AppScan Source. http:\/\/www-03.ibm.com\/software\/products\/en\/appscan-source"},{"key":"263_CR3","unstructured":"Kausler Suite. https:\/\/github.com\/BoiseState\/string-constraint-solvers"},{"key":"263_CR4","unstructured":"LibStranger. https:\/\/github.com\/vlab-cs-ucsb\/LibStranger"},{"key":"263_CR5","unstructured":"Personal communications with the Stranger team. 2015"},{"key":"263_CR6","doi-asserted-by":"publisher","unstructured":"Abdulla PA, Atig MF, Chen Y-F, Hol\u00edk L, Rezine A, R\u00fcmmer P, Stenman J (2014) String constraints for verification. In: Proceedings of the 26th international conference on computer aided verification, CAV\u201914, pp 150\u2013166","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"263_CR7","unstructured":"Barrett C, Fontaine P, Tinelli C (2016) The Satisfiability Modulo Theories Library (SMT-LIB). http:\/\/www.SMT-LIB.org"},{"key":"263_CR8","doi-asserted-by":"publisher","unstructured":"Bj\u00f8rner N, Tillmann N, Voronkov A (2009) Path feasibility analysis for string-manipulating programs. In: Proceedings of the 15th international conference on tools and algorithms for the construction and analysis of systems, TACAS \u201909, pp 307\u2013321","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"263_CR9","unstructured":"Cristian C, Daniel D, Dawson E (2008) Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In: Proceedings of the 8th USENIX conference on operating systems design and implementation, OSDI\u201908. USENIX Association, Berkeley, pp 209\u2013224"},{"key":"263_CR10","doi-asserted-by":"publisher","unstructured":"Chipounov V, Kuznetsov V, Candea G (2011) S2e: a platform for in-vivo multi-path analysis of software systems. In: Proceedings of the sixteenth international conference on architectural support for programming languages and operating systems. ASPLOS XVI. ACM, New York, pp 265\u2013278","DOI":"10.1145\/1950365.1950396"},{"key":"263_CR11","doi-asserted-by":"publisher","unstructured":"Christensen AS, M\u00f8ller A, Schwartzbach MI (2003) Precise analysis of string expressions. In: Proceedings of the 10th international conference on static analysis, SAS\u201903, pp 1\u201318","DOI":"10.7146\/brics.v10i5.21776"},{"key":"263_CR12","doi-asserted-by":"publisher","unstructured":"De\u00a0Moura L, Bj\u00f8rner N (2008) Z3: an efficient smt solver. In: Proceedings of the theory and practice of software, 14th international conference on Tools and algorithms for the construction and analysis of systems, TACAS\u201908, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"263_CR13","doi-asserted-by":"publisher","unstructured":"Ganesh V, Dill DL (2007) A decision procedure for bit-vectors and arrays. In: Proceedings of the 19th international conference on computer aided verification, CAV\u201907, pp 519\u2013531","DOI":"10.1007\/978-3-540-73368-3_52"},{"key":"263_CR14","doi-asserted-by":"crossref","unstructured":"Ganesh V, Minnes M, Solar-Lezama A, Rinard M (2012) Word equations with length constraints: what\u2019s decidable? In: HVC\u201912","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"263_CR15","doi-asserted-by":"publisher","unstructured":"Ghosh I, Shafiei N, Li G, Chiang W-F (2013) JST: an automatic test generation tool for industrial java applications with strings. In: Proceedings of the 2013 international conference on software engineering, ICSE \u201913, pp 992\u20131001","DOI":"10.1109\/ICSE.2013.6606649"},{"key":"263_CR16","doi-asserted-by":"publisher","unstructured":"Hooimeijer P, Weimer W (2010) Solving string constraints lazily. In: Proceedings of the IEEE\/ACM international conference on automated software engineering, ASE \u201910, pp 377\u2013386","DOI":"10.1145\/1858996.1859080"},{"key":"263_CR17","volume-title":"Introduction to automata theory, languages, and computation","author":"JE Hopcroft","year":"2007","unstructured":"Hopcroft JE, Motwani R, Ullman JD (2007) Introduction to automata theory, languages, and computation. Pearson\/Addison Wesley, Reading"},{"key":"263_CR18","doi-asserted-by":"publisher","unstructured":"Jeon J, Qiu X, Fetter-Degges J, Foster JS, Solar-Lezama A (2016) Synthesizing framework models for symbolic execution. In: Proceedings of the 38th international conference on software engineering, ICSE \u201916. ACM, New York, pp 156\u2013167","DOI":"10.1145\/2884781.2884856"},{"key":"263_CR19","doi-asserted-by":"publisher","unstructured":"Je\u017c A (2013) Recompression: word equations and beyond. In: Developments in language theory, Lecture Notes in Computer Science, pp 12\u201326","DOI":"10.1007\/978-3-642-38771-5_2"},{"issue":"3","key":"263_CR20","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/337244.337255","volume":"47","author":"J Karhum\u00e4ki","year":"2000","unstructured":"Karhum\u00e4ki J, Mignosi F, Plandowski W (2000) The expressibility of languages and relations by word equations. J ACM 47(3):483\u2013505","journal-title":"J ACM"},{"key":"263_CR21","doi-asserted-by":"crossref","unstructured":"Kausler S (2014) Evaluation of string constraint solvers using dynamic symbolic execution. Master\u2019s Thesis, Boise State University","DOI":"10.1145\/2642937.2643003"},{"key":"263_CR22","doi-asserted-by":"publisher","unstructured":"Kausler S, Sherman E (2014) Evaluation of string constraint solvers in the context of symbolic execution. In: Proceedings of the 29th ACM\/IEEE international conference on automated software engineering, ASE \u201914. ACM, New York, pp 259\u2013270","DOI":"10.1145\/2642937.2643003"},{"key":"263_CR23","doi-asserted-by":"publisher","unstructured":"Kiezun A, Ganesh V, Guo PJ, Hooimeijer P, Ernst MD (2009) Hampi: a solver for string constraints. In: Proceedings of the eighteenth international symposium on software testing and analysis, ISSTA \u201909, pp 105\u2013116","DOI":"10.1145\/1572272.1572286"},{"key":"263_CR24","doi-asserted-by":"publisher","unstructured":"Li G, Andreasen E, Ghosh I (2014) SymJS: automatic symbolic testing of javascript web applications. In: Proceedings of the 22Nd ACM SIGSOFT international symposium on foundations of software engineering, FSE 2014, pp 449\u2013459","DOI":"10.1145\/2635868.2635913"},{"key":"263_CR25","doi-asserted-by":"publisher","unstructured":"Li G, Ghosh I (2013) PASS: string solving with parameterized array and interval automaton. In: 9th international Haifa verification conference, HVC \u201913, pp 15\u201331","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"263_CR26","doi-asserted-by":"publisher","unstructured":"Liang T, Reynolds A, Tinelli C, Barrett C, Deters M (2014) A dpll(t) theory solver for a theory of strings and regular expressions. In: Proceedings of the 26th international conference on computer aided verification, CAV\u201914, pp 646\u2013662","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"263_CR27","doi-asserted-by":"crossref","unstructured":"Makanin GS (1977) The problem of solvability of equations in a free semigroup. Math Sbornik 103:147\u2013236 (1977). English transl. in Math USSR Sbornik 32","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"263_CR28","unstructured":"Matiyasevich Y (2007) Word equations, Fibonacci numbers, and Hilbert\u2019s tenth problem. In: Workshop on Fibonacci words"},{"issue":"3","key":"263_CR29","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W Plandowski","year":"2004","unstructured":"Plandowski W (2004) Satisfiability of word equations with constants is in pspace. J ACM 51(3):483\u2013496","journal-title":"J ACM"},{"key":"263_CR30","doi-asserted-by":"publisher","unstructured":"Plandowski W (2006) An efficient algorithm for solving word equations. In: Proceedings of the 38th annual ACM symposium on theory of computing, STOC \u201906, pp 467\u2013476","DOI":"10.1145\/1132516.1132584"},{"key":"263_CR31","doi-asserted-by":"publisher","unstructured":"Qu X, Robinson B (2011) A case study of concolic testing tools and their limitations. In: 2011 international symposium on empirical software engineering and measurement (ESEM). IEEE Computer Society, pp 117\u2013126","DOI":"10.1109\/ESEM.2011.20"},{"key":"263_CR32","doi-asserted-by":"publisher","unstructured":"Redelinghuys G, Visser W, Geldenhuys J (2012) Symbolic execution of programs with strings. In: Proceedings of the South African Institute for computer scientists and information technologists conference, SAICSIT \u201912, pp 139\u2013148","DOI":"10.1145\/2389836.2389853"},{"key":"263_CR33","doi-asserted-by":"publisher","unstructured":"Saxena P, Akhawe D, Hanna S, Mao F, McCamant S, Song D (2010) A symbolic execution framework for javascript. In: Proceedings of the 2010 IEEE symposium on security and privacy, SP \u201910, pp 513\u2013528","DOI":"10.1109\/SP.2010.38"},{"key":"263_CR34","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/3-540-55124-7_4","volume-title":"Word equations and related topics, Lecture Notes in Computer Science","author":"K Schulz","year":"1992","unstructured":"Schulz K (1992) Makanin\u2019s algorithm for word equations-two improvements and a generalization. In: Schulz K (ed) Word equations and related topics, Lecture Notes in Computer Science, vol 572. Springer, Berlin, pp 85\u2013150"},{"issue":"4","key":"263_CR35","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/2522920.2522926","volume":"22","author":"T Tateishi","year":"2013","unstructured":"Tateishi T, Pistoia M, Tripp O (2013) Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans Softw Eng Methodol 22(4):33:1\u201333:33","journal-title":"ACM Trans Softw Eng Methodol"},{"key":"263_CR36","doi-asserted-by":"publisher","unstructured":"Trinh M-T, Chu D-H, Jaffar J (2014) S3: a symbolic string solver for vulnerability detection in web applications. In: Proceedings of the 2014 ACM SIGSAC conference on computer and communications security, CCS \u201914, pp 1232\u20131243","DOI":"10.1145\/2660267.2660372"},{"key":"263_CR37","doi-asserted-by":"publisher","unstructured":"Xie X, Liu Y, Le W, Li X, Chen H (2015) S-looper: automatic summarization for multipath string loops. In: Proceedings of the 2015 international symposium on software testing and analysis, ISSTA 2015. ACM, New York, pp 188\u2013198","DOI":"10.1145\/2771783.2771815"},{"key":"263_CR38","doi-asserted-by":"publisher","unstructured":"Yu F, Alkhalaf M, Bultan T (2010) Stranger: an automata-based string analysis tool for php. In: Proceedings of the 16th international conference on tools and algorithms for the construction and analysis of systems, TACAS\u201910, pp 154\u2013157","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"263_CR39","doi-asserted-by":"publisher","unstructured":"Yu F, Bultan T, Ibarra OH (2009) Symbolic string verification: combining string analysis and size analysis. In: Proceedings of the 15th international conference on tools and algorithms for the construction and analysis of systems, TACAS \u201909, pp 322\u2013336","DOI":"10.1007\/978-3-642-00768-2_28"},{"key":"263_CR40","doi-asserted-by":"crossref","unstructured":"Zheng Y, Ganesh V, Subramanian S, Tripp O, Dolby J, Zhang X (2015) Effective search-space pruning for solvers of string equations, regular expressions and length constraints. Technical report. https:\/\/sites.google.com\/site\/z3strsolver\/publications","DOI":"10.1007\/978-3-319-21690-4_14"},{"key":"263_CR41","doi-asserted-by":"publisher","unstructured":"Zheng Y, Zhang X, Ganesh V (2013) Z3-str: a z3-based string solver for web application analysis. In: Proceedings of the 2013 9th joint meeting on foundations of software engineering, ESEC\/FSE 2013, pp 114\u2013124","DOI":"10.1145\/2491411.2491456"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0263-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0263-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0263-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,16]],"date-time":"2019-09-16T20:18:13Z","timestamp":1568665093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0263-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,12,27]]},"references-count":41,"journal-issue":{"issue":"2-3","published-print":{"date-parts":[[2017,6]]}},"alternative-id":["263"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0263-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,12,27]]}}}