{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:58:02Z","timestamp":1776333482363,"version":"3.51.2"},"reference-count":35,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T00:00:00Z","timestamp":1459814400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T00:00:00Z","timestamp":1459814400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1228765"],"award-info":[{"award-number":["1228765"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000083","name":"Directorate for Computer and Information Science and Engineering","doi-asserted-by":"publisher","award":["1228768"],"award-info":[{"award-number":["1228768"]}],"id":[{"id":"10.13039\/100000083","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2016,6]]},"DOI":"10.1007\/s10703-016-0247-6","type":"journal-article","created":{"date-parts":[[2016,4,5]],"date-time":"2016-04-05T15:31:49Z","timestamp":1459870309000},"page":"206-234","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":42,"title":["An efficient SMT solver for string constraints"],"prefix":"10.1007","volume":"48","author":[{"given":"Tianyi","family":"Liang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nestan","family":"Tsiskaridze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6726-775X","authenticated-orcid":false,"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,4,5]]},"reference":[{"key":"247_CR1","doi-asserted-by":"crossref","unstructured":"Abdulla PA, Atig MF, Chen YF, Holik L, Rezine A, Rummer P, Stenman J (2014) String constraints for verification. In: Biere A, Bloem R (eds) Proceedings of the 26th international conference on computer aided verification. Lecture notes in computer science, vol. 8559. Springer, Berlin","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"247_CR2","doi-asserted-by":"crossref","unstructured":"Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: Proceedings of LPAR\u201906. Lecture notes in computer science, vol. 4246. Springer, Berlin, pp 512\u2013526","DOI":"10.1007\/11916277_35"},{"key":"247_CR3","doi-asserted-by":"crossref","unstructured":"Barrett C, Sebastiani R, Seshia S, Tinelli C (2009) Satisfiability modulo theories. In: Biere A, Heule MJH, van Maaren H, Walsh T (eds) Handbook of satisfiability, vol 185, chap 26. IOS Press, Amsterdam, pp 825\u2013885","DOI":"10.3233\/978-1-58603-929-5-825"},{"key":"247_CR4","doi-asserted-by":"crossref","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. Lecture notes in computer science. Springer, pp 307\u2013321","DOI":"10.1007\/978-3-642-00768-2_27"},{"key":"247_CR5","unstructured":"Brumley D, Caballero J, Liang Z, Newsome J (2007) Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation. In: Proceedings of the 16th USENIX security symposium, Boston, MA, USA, 6\u201310 August 2007"},{"key":"247_CR6","doi-asserted-by":"crossref","unstructured":"Brumley D, Wang H, Jha S, Song DX (2007) Creating vulnerability signatures using weakest preconditions. In: 20th IEEE computer security foundations symposium, CSF 2007, 6\u20138 July 2007, Venice, Italy, pp 311\u2013325","DOI":"10.1109\/CSF.2007.17"},{"key":"247_CR7","doi-asserted-by":"crossref","unstructured":"Christensen AS, M\u00f8ller A, Schwartzbach MI (2003) Precise analysis of string expressions. In: Proceedings of the 10th international conference on static analysis. Lecture notes in computer science. Springer, Berlin, pp 1\u201318","DOI":"10.1007\/3-540-44898-5_1"},{"key":"247_CR8","doi-asserted-by":"crossref","unstructured":"De Moura 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. Lecture notes in computer science. Springer, Berlin, pp 337\u2013340","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"247_CR9","unstructured":"Egele M, Kruegel C, Kirda E, Yin H, Song D (2007) Dynamic spyware analysis. In: 2007 USENIX annual technical conference on proceedings of the USENIX annual technical conference, ATC\u201907. USENIX Association, Berkeley, CA, USA, pp 18:1\u201318:14"},{"key":"247_CR10","unstructured":"Fu X, Li C (2010) A string constraint solver for detecting web application vulnerability. In: Proceedings of the 22nd international conference on software engineering and knowledge engineering, SEKE\u20192010. Knowledge Systems Institute Graduate School, Skokie"},{"key":"247_CR11","unstructured":"Ganesh V, Minnes M, Solar-Lezama A, Rinard M (2013) Word equations with length constraints: what\u2019s decidable? In: Proceedings of the 8th international conference on hardware and software: verification and testing, HVC\u201912. Springer, Berlin, pp 209\u2013226"},{"key":"247_CR12","doi-asserted-by":"crossref","unstructured":"Ghosh I, Shafiei N, Li G, Chiang W (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. IEEE Press, Piscataway, pp. 992\u20131001","DOI":"10.1109\/ICSE.2013.6606649"},{"key":"247_CR13","doi-asserted-by":"crossref","unstructured":"Hooimeijer P, Veanes M (2011) An evaluation of automata algorithms for string analysis. In: Proceedings of the 12th international conference on verification, model checking, and abstract interpretation. Springer, Berlin, pp 248\u2013262","DOI":"10.1007\/978-3-642-18275-4_18"},{"key":"247_CR14","doi-asserted-by":"crossref","unstructured":"Hooimeijer P, Weimer W (2009) A decision procedure for subset constraints over regular languages. In: Proceedings of the 2009 ACM SIGPLAN conference on programming language design and implementation. ACM, Dublin, pp 188\u2013198","DOI":"10.1145\/1542476.1542498"},{"key":"247_CR15","doi-asserted-by":"crossref","unstructured":"Hooimeijer P, Weimer W (2010) Solving string constraints lazily. In: Proceedings of the IEEE\/ACM international conference on automated software engineering. ACM, New York, pp 377\u2013386","DOI":"10.1145\/1858996.1859080"},{"key":"247_CR16","doi-asserted-by":"crossref","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. ACM, New York, pp 105\u2013116","DOI":"10.1145\/1572272.1572286"},{"key":"247_CR17","doi-asserted-by":"crossref","unstructured":"Li G, Ghosh I (2013) PASS: string solving with parameterized array and interval automaton. In: Bertacco V, Legay A (eds) Hardware and software: verification and testing. Lecture notes in computer science, vol 8244. Springer, Berlin, pp 15\u201331","DOI":"10.1007\/978-3-319-03077-7_2"},{"key":"247_CR18","doi-asserted-by":"crossref","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: Biere A, Bloem R (eds) Proceedings of the 26th international conference on computer aided verification. Lecture notes in computer science, vol 8559. Springer, Berlin","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"247_CR19","doi-asserted-by":"crossref","unstructured":"Liang T, Tsiskaridze N, Reynolds A, Tinelli C, Barrett C (2015) A decision procedure for regular membership and length constraints over unbounded strings. In: Frontiers of combining systems. Springer, Berlin, pp 135\u2013150","DOI":"10.1007\/978-3-319-24246-0_9"},{"key":"247_CR20","doi-asserted-by":"crossref","unstructured":"Makanin GS (1977) The problem of solvability of equations in a free semigroup. English transl. in Math USSR Sbornik, vol 32, pp 147\u2013236","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"247_CR21","unstructured":"Namjoshi KS, Narlikar GJ (2010) Robust and fast pattern matching for intrusion detection. In: INFOCOM 2010. 29th IEEE international conference on computer communications, joint conference of the IEEE computer and communications societies, 15\u201319 March 2010, San Diego, CA, USA, pp 740\u2013748"},{"issue":"2","key":"247_CR22","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen DC (1979) Simplification by cooperating decision procedures. ACM Trans Program Lang Syst 1(2):245\u2013257","journal-title":"ACM Trans Program Lang Syst"},{"issue":"6","key":"247_CR23","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT Modulo theories: from an abstract Davis\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J ACM 53(6):937\u2013977","journal-title":"J ACM"},{"key":"247_CR24","first-page":"275","volume-title":"Resolution of equations in algebraic structures","author":"D Perrin","year":"1989","unstructured":"Perrin D (1989) Equations in words. In: Ait-Kaci H, Nivat M (eds) Resolution of equations in algebraic structures, vol 2. Academic Press, Cambridge, pp 275\u2013298"},{"issue":"3","key":"247_CR25","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":"247_CR26","unstructured":"Saxena P, Akhawe D (2010) Kaluza web site. http:\/\/webblaze.cs.berkeley.edu\/2010\/kaluza\/"},{"key":"247_CR27","doi-asserted-by":"crossref","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. IEEE Computer Society, pp 513\u2013528","DOI":"10.1109\/SP.2010.38"},{"key":"247_CR28","doi-asserted-by":"crossref","unstructured":"Stump A, Sutcliffe G, Tinelli C (2014) Starexec: a cross-community infrastructure for logic solving. In: Demri S, Kapur D, Weidenbach C (eds) Proceedings of the 7th international joint conference on automated reasoning. Lecture notes in artificial intelligence. Springer, Berlin","DOI":"10.1007\/978-3-319-08587-6_28"},{"key":"247_CR29","doi-asserted-by":"crossref","unstructured":"Tillmann N, Halleux J (2008) Pex\u2014white box test generation for .NET. In Beckert B, H\u00e4hnle R (eds) Tests and proofs. Lecture notes in computer science, vol 4966. Springer, Berlin, pp 134\u2013153","DOI":"10.1007\/978-3-540-79124-9_10"},{"key":"247_CR30","doi-asserted-by":"crossref","unstructured":"Tinelli C, Harandi MT (1996) A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Baader F, Schulz KU (eds) Frontiers of combining systems: proceedings of the 1st international workshop (Munich, Germany). Applied logic. Kluwer Academic Publishers, Dordrecht, pp 103\u2013120","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"247_CR31","doi-asserted-by":"crossref","unstructured":"Trinh MT, Chu DH, Jaffar J (2014) S3: a symbolic string solver for vulnerability detection in web applications. In: Yung M, Li N (eds) Proceedings of the 21st ACM conference on computer and communications security. ACM, New York, pp 1232\u20131243","DOI":"10.1145\/2660267.2660372"},{"key":"247_CR32","doi-asserted-by":"crossref","unstructured":"Veanes M (2013) Applications of symbolic finite automata. In: Proceedings of the 18th international conference on implementation and application of automata, CIAA\u201913. Springer, Berlin, pp 16\u201323","DOI":"10.1007\/978-3-642-39274-0_3"},{"key":"247_CR33","doi-asserted-by":"crossref","unstructured":"Veanes M, Bj\u00f8rner N, De Moura L (2010) Symbolic automata constraint solving. In: Proceedings of the 17th international conference on logic for programming, artificial intelligence, and reasoning. Lecture notes in computer science. Springer, Berlin, pp 640\u2013654","DOI":"10.1007\/978-3-642-16242-8_45"},{"key":"247_CR34","doi-asserted-by":"crossref","unstructured":"Yu F, Alkhalaf M, Bultan T (2010) Stranger: an automata-based string analysis tool for php. In: Esparza J, Majumdar R (eds) Tools and algorithms for the construction and analysis of systems. Lecture notes in computer science, vol 6015. Springer, Berlin, pp 154\u2013157","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"247_CR35","doi-asserted-by":"crossref","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. ACM, New York, 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-0247-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-016-0247-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-0247-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-016-0247-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,2]],"date-time":"2025-06-02T05:05:23Z","timestamp":1748840723000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-016-0247-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,4,5]]},"references-count":35,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2016,6]]}},"alternative-id":["247"],"URL":"https:\/\/doi.org\/10.1007\/s10703-016-0247-6","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,4,5]]},"assertion":[{"value":"5 April 2016","order":1,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}