{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T10:23:34Z","timestamp":1770287014742,"version":"3.49.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319242453","type":"print"},{"value":"9783319242460","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_9","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"135-150","source":"Crossref","is-referenced-by-count":29,"title":["A Decision Procedure for Regular Membership and Length Constraints over Unbounded Strings"],"prefix":"10.1007","author":[{"given":"Tianyi","family":"Liang","sequence":"first","affiliation":[]},{"given":"Nestan","family":"Tsiskaridze","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"9_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"150","DOI":"10.1007\/978-3-319-08867-9_10","volume-title":"Computer Aided Verification","author":"P.A. Abdulla","year":"2014","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y.-F., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: String constraints for verification. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 150\u2013166. Springer, Heidelberg (2014)"},{"issue":"2","key":"9_CR2","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(95)00182-4","volume":"155","author":"V. Antimirov","year":"1996","unstructured":"Antimirov, V.: Partial derivatives of regular expressions and finite automaton constructions. Theor. Comput. Sci.\u00a0155(2), 291\u2013319 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"653","DOI":"10.1007\/978-3-642-15155-2_57","volume-title":"Mathematical Foundations of Computer Science 2010","author":"B. Badban","year":"2010","unstructured":"Badban, B., Dashti, M.: Semi-linear parikh images of regular expressions via reduction. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 653\u2013664. Springer, Heidelberg (2010)"},{"key":"9_CR5","unstructured":"Barrett, C., Sebastiani, R., Seshia, S., Tinelli, C.: Satisfiability modulo theories. In: Biere, A., Heule, M.J.H., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability, vol.\u00a0185, chapter 26, pp. 825\u2013885. IOS Press, February 2008"},{"issue":"1","key":"9_CR6","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/0304-3975(86)90088-5","volume":"48","author":"G. Berry","year":"1986","unstructured":"Berry, G., Sethi, R.: From regular expressions to deterministic automata. Theor. Comput. Sci.\u00a048(1), 117\u2013126 (1986)","journal-title":"Theor. Comput. Sci."},{"key":"9_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"307","DOI":"10.1007\/978-3-642-00768-2_27","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: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 307\u2013321. Springer, Heidelberg (2009)"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-44898-5_1","volume-title":"Static Analysis","author":"A.S. Christensen","year":"2003","unstructured":"Christensen, A.S., M\u00f8ller, A., Schwartzbach, M.I.: Precise analysis of string expressions. In: Cousot, R. (ed.) SAS 2003. LNCS, vol.\u00a02694, pp. 1\u201318. Springer, Heidelberg (2003)"},{"key":"9_CR9","unstructured":"Fu, X., Chih Li, C.: A string constraint solver for detecting web application vulnerability. In: Proceedings of the 22nd International Conference on Software Engineering and Knowledge Engineering, SEKE 2010. Knowledge Systems Institute Graduate (2010)"},{"key":"9_CR10","first-page":"992","volume-title":"Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013","author":"I. Ghosh","year":"2013","unstructured":"Ghosh, I., Shafiei, N., Li, G., Chiang, W.-F.: JST: An automatic test generation tool for industrial Java applications with strings. In: Proceedings of the 2013 International Conference on Software Engineering, ICSE 2013, pp. 992\u20131001. IEEE Press, Piscataway (2013)"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/3-540-60630-0_5","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.G. Henriksen","year":"1995","unstructured":"Henriksen, J.G., Jensen, J.L., J\u00f8rgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol.\u00a01019, pp. 89\u2013110. Springer, Heidelberg (1995)"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 248\u2013262. Springer, Heidelberg (2011)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: A decision procedure for subset constraints over regular languages. In: Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, pp. 188\u2013198. ACM (2009)","DOI":"10.1145\/1542476.1542498"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Hooimeijer, P., Weimer, W.: Solving string constraints lazily. In: Proceedings of the IEEE\/ACM International Conference on Automated Software Engineering, pp. 377\u2013386. ACM (2010)","DOI":"10.1145\/1858996.1859080"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"Kiezun, A., Ganesh, V., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: a solver for string constraints. In: Proceedings of the Eighteenth International Symposium on Software Testing and Analysis, pp. 105\u2013116. ACM (2009)","DOI":"10.1145\/1572272.1572286"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/3-540-44674-5_15","volume-title":"Implementation and Application of Automata","author":"N. Klarlund","year":"2001","unstructured":"Klarlund, N., M\u00f8ller, A.: MONA implementation secrets. In: Yu, S., P\u0103un, A. (eds.) CIAA 2000. LNCS, vol.\u00a02088, pp. 182\u2013194. Springer, Heidelberg (2001)"},{"key":"9_CR17","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Lower bounds for natural proof systems. In: FOCS, pp. 254\u2013266. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.16"},{"key":"9_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1007\/978-3-319-03077-7_2","volume-title":"Hardware and Software: Verification and Testing","author":"G. Li","year":"2013","unstructured":"Li, G., Ghosh, I.: PASS: String solving with parameterized array and interval automaton. In: Bertacco, V., Legay, A. (eds.) HVC 2013. LNCS, vol.\u00a08244, pp. 15\u201331. Springer, Heidelberg (2013)"},{"key":"9_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"646","DOI":"10.1007\/978-3-319-08867-9_43","volume-title":"Computer Aided Verification","author":"T. Liang","year":"2014","unstructured":"Liang, T., Reynolds, A., Tinelli, C., Barrett, C., Deters, M.: A dPLL(T) theory solver for a theory of strings and regular expressions. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol.\u00a08559, pp. 646\u2013662. Springer, Heidelberg (2014)"},{"key":"9_CR20","unstructured":"Liang, T., Tsiskaridze, N., Reynolds, A., Tinelli, C., Barrett, C.: A decision procedure for regular membership and length constraints over unbounded strings. Technical report, Department of Computer Science, The University of Iowa (2015). \n                      \n                        http:\/\/www.cs.uiowa.edu\/~tinelli\/papers.html"},{"key":"9_CR21","unstructured":"Lu, K.Z.M.: XHaskell - Adding Regular Expression Type to Haskell. PhD thesis, National University of Singapore (2009)"},{"key":"9_CR22","first-page":"147","volume":"32","author":"G.S. Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. English Rransl. in Math USSR Sbornik\u00a032, 147\u2013236 (1977)","journal-title":"English Rransl. in Math USSR Sbornik"},{"key":"9_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"310","DOI":"10.1007\/11494645_39","volume-title":"New Computational Paradigms","author":"Y.V. Matiyasevich","year":"2005","unstructured":"Matiyasevich, Y.V.: Hilbert\u2019s tenth problem and paradigms of computation. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) CiE 2005. LNCS, vol.\u00a03526, pp. 310\u2013321. Springer, Heidelberg (2005)"},{"issue":"4","key":"9_CR24","doi-asserted-by":"publisher","first-page":"570","DOI":"10.1145\/321356.321364","volume":"13","author":"R.J. Parikh","year":"1966","unstructured":"Parikh, R.J.: On context-free languages. J. ACM\u00a013(4), 570\u2013581 (1966)","journal-title":"J. ACM"},{"issue":"3","key":"9_CR25","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1145\/990308.990312","volume":"51","author":"W. Plandowski","year":"2004","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in pspace. J. ACM\u00a051(3), 483\u2013496 (2004)","journal-title":"J. ACM"},{"key":"9_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-44881-0_35","volume-title":"Rewriting Techniques and Applications","author":"G. Rosu","year":"2003","unstructured":"Rosu, G., Viswanathan, M.: Testing extended regular language membership incrementally by rewriting. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 499\u2013514. Springer, Heidelberg (2003)"},{"key":"9_CR27","volume-title":"Word Equations and Related Topics","year":"1990","unstructured":"Schulz, K. (ed.): Word Equations and Related Topics. Springer-Verlag New York, Inc., New York (1990)"},{"key":"9_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/2522920.2522926","volume":"33","author":"T. Tateishi","year":"2013","unstructured":"Tateishi, T., Pistoia, M., Tripp, O.: Path- and index-sensitive string analysis based on monadic second-order logic. ACM Trans. Softw. Eng. Methodol.\u00a033, 1\u201333 (2013)","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"134","DOI":"10.1007\/978-3-540-79124-9_10","volume-title":"Tests and Proofs","author":"N. Tillmann","year":"2008","unstructured":"Tillmann, N., de Halleux, J.: Pex\u2013white box test generation for.NET. In: Beckert, B., H\u00e4hnle, R. (eds.) TAP 2008. LNCS, vol.\u00a04966, pp. 134\u2013153. Springer, Heidelberg (2008)"},{"key":"9_CR30","doi-asserted-by":"crossref","unstructured":"Trinh, M.-T., Chu, D.-H., Jaffar, J.: 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 (2014)","DOI":"10.1145\/2660267.2660372"},{"key":"9_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"16","DOI":"10.1007\/978-3-642-39274-0_3","volume-title":"Proceedings of the 18th International Conference on Implementation and Application of Automata, CIAA 2013","author":"M. Veanes","year":"2013","unstructured":"Veanes, M.: Applications of symbolic finite automata. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol.\u00a07982, pp. 16\u201323. Springer, Heidelberg (2013)"},{"key":"9_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/978-3-642-16242-8_45","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"M. Veanes","year":"2010","unstructured":"Veanes, M., Bj\u00f8rner, N., de Moura, L.: Symbolic automata constraint solving. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 640\u2013654. Springer, Heidelberg (2010)"},{"key":"9_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"154","DOI":"10.1007\/978-3-642-12002-2_13","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"F. Yu","year":"2010","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: An automata-based string analysis tool for PHP. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 154\u2013157. Springer, Heidelberg (2010)"},{"key":"9_CR34","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/2491411.2491456","volume-title":"Proceedings of the 2013 9th Joint Meeting on Foundations of Software Engineering, ESEC\/FSE 2013","author":"Y. Zheng","year":"2013","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: 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. ACM, New York (2013)"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,31]],"date-time":"2019-05-31T00:36:29Z","timestamp":1559262989000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}