{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,14]],"date-time":"2026-03-14T09:01:52Z","timestamp":1773478912585,"version":"3.50.1"},"reference-count":26,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T00:00:00Z","timestamp":1698105600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T00:00:00Z","timestamp":1698105600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2024,3]]},"DOI":"10.1007\/s00236-023-00446-4","type":"journal-article","created":{"date-parts":[[2023,10,24]],"date-time":"2023-10-24T09:04:33Z","timestamp":1698138273000},"page":"23-52","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["A decision procedure for string constraints with string\/integer conversion and flat regular constraints"],"prefix":"10.1007","volume":"61","author":[{"given":"Hao","family":"Wu","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yu-Fang","family":"Chen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Zhilin","family":"Wu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bican","family":"Xia","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Naijun","family":"Zhan","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,24]]},"reference":[{"key":"446_CR1","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Dolby, J., Janku, P., Lin, H., Hol\u00edk, L., Wu, W.: Efficient handling of string-number conversion. In: Proceedings of the 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI\u201920, pp. 943\u2013957. ACM, New York, NY, US (2020). https:\/\/doi.org\/10.1145\/3385412.3386034","DOI":"10.1145\/3385412.3386034"},{"key":"446_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P.: Flatten and conquer: a framework for efficient analysis of string constraints. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI\u201917, pp. 602\u2013617. ACM, New York, NY, US (2017). https:\/\/doi.org\/10.1145\/3062341.3062384","DOI":"10.1145\/3062341.3062384"},{"key":"446_CR3","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Diep, B.P., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P.: Trau: SMT solver for string constraints. In: Bj\u00f8rner, N.S., Gurfinkel, A. (eds.) Formal Methods in Computer Aided Design, FMCAD\u201918, pp. 1\u20135. IEEE, Washington, DC (2018). https:\/\/doi.org\/10.23919\/FMCAD.2018.8602997","DOI":"10.23919\/FMCAD.2018.8602997"},{"key":"446_CR4","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Chen, Y., Hol\u00edk, L., Rezine, A., R\u00fcmmer, P., Stenman, J.: Norn: An SMT solver for string constraints. In: Computer Aided Verification - 27th International Conference, CAV\u201915. Lecture Notes in Computer Science, vol. 9206, pp. 462\u2013469. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_29","DOI":"10.1007\/978-3-319-21690-4_29"},{"key":"446_CR5","doi-asserted-by":"publisher","unstructured":"Aydin, A., Eiers, W., Bang, L., Brennan, T., Gavrilov, M., Bultan, T., Yu, F.: Parameterized model counting for string and numeric constraints. In: Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC\/SIGSOFT FSE\u201918, pp. 400\u2013410. ACM, New York, NY, USA (2018). https:\/\/doi.org\/10.1145\/3236024.3236064","DOI":"10.1145\/3236024.3236064"},{"key":"446_CR6","doi-asserted-by":"publisher","unstructured":"Barrett, C.W., Conway, C.L., Deters, M., Hadarean, L., Jovanovic, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Computer Aided Verification - 23rd International Conference, CAV\u201911. Lecture Notes in Computer Science, vol. 6806, pp. 171\u2013177. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14","DOI":"10.1007\/978-3-642-22110-1_14"},{"key":"446_CR7","doi-asserted-by":"publisher","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z.: What is decidable about string constraints with the replace all function. In: Proceedings of the ACM on Programming Languages 2(POPL), 3\u20131329 (2018) https:\/\/doi.org\/10.1145\/3158091","DOI":"10.1145\/3158091"},{"key":"446_CR8","unstructured":"Cherlin, G., Point, F.: On extensions of presburger arithmetic. In: Proceedings of the Fourth Easter Conference on Model Theory, Gross Koris, pp. 17\u201334 (1986). https:\/\/webusers.imj-prg.fr\/%7efrancoise.point\/papiers\/cherlin_point86.pdf"},{"key":"446_CR9","first-page":"91","volume":"7","author":"DC Cooper","year":"1972","unstructured":"Cooper, D.C.: Theorem proving in arithmetic without multiplication. Mach. Intell. 7, 91\u2013100 (1972)","journal-title":"Mach. Intell."},{"key":"446_CR10","doi-asserted-by":"publisher","unstructured":"Day, J.D., Ganesh, V., He, P., Manea, F., Nowotka, D.: The satisfiability of word equations: Decidable and undecidable theories. In: Reachability Problems - 12th International Conference, RP\u201918. Lecture Notes in Computer Science, vol. 11123, pp. 15\u201329. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00250-3_2","DOI":"10.1007\/978-3-030-00250-3_2"},{"key":"446_CR11","unstructured":"ECMAScript, E., Association, E.C.M., et al.: ECMAScript language specification (2019). https:\/\/www.ecma-international.org\/ecma-262\/"},{"key":"446_CR12","doi-asserted-by":"publisher","unstructured":"Haase, C.: Subclasses of presburger arithmetic and the weak EXP hierarchy. In: Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS \u201914, Vienna, Austria, July 14\u201318, 2014, pp. 47\u201314710. ACM, New York, NY, US (2014). https:\/\/doi.org\/10.1145\/2603088.2603092","DOI":"10.1145\/2603088.2603092"},{"key":"446_CR13","doi-asserted-by":"publisher","DOI":"10.1093\/oso\/9780199219858.001.0001","volume-title":"An Introduction to the Theory of Numbers","author":"GH Hardy","year":"2008","unstructured":"Hardy, G.H., Wright, E.M.: An Introduction to the Theory of Numbers, 6th edn. Clarendon Press, Oxford (2008)","edition":"6"},{"key":"446_CR14","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Janku, P., Lin, A.W., R\u00fcmmer, P., Vojnar, T.: String constraints with concatenation and transducers solved efficiently. In: Proceedings of the ACM on Programming Languages 2(POPL), 4\u20131432 (2018) https:\/\/doi.org\/10.1145\/3158092","DOI":"10.1145\/3158092"},{"issue":"4","key":"446_CR15","doi-asserted-by":"publisher","first-page":"25","DOI":"10.1145\/2377656.2377662","volume":"21","author":"A Kiezun","year":"2012","unstructured":"Kiezun, A., Ganesh, V., Artzi, S., Guo, P.J., Hooimeijer, P., Ernst, M.D.: HAMPI: A solver for word equations over strings, regular expressions, and context-free grammars. ACM Trans. Softw. Eng. Methodol. 21(4), 25\u201312528 (2012). https:\/\/doi.org\/10.1145\/2377656.2377662","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"446_CR16","doi-asserted-by":"publisher","unstructured":"Li, G., Ghosh, I.: PASS: string solving with parameterized array and interval automaton. In: Hardware and Software: Verification and Testing - 9th International Haifa Verification Conference, HVC\u201913. Lecture Notes in Computer Science, vol. 8244, pp. 15\u201331. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03077-7_2","DOI":"10.1007\/978-3-319-03077-7_2"},{"issue":"2","key":"446_CR17","first-page":"147","volume":"145","author":"GS Makanin","year":"1977","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147\u2013236 (1977)","journal-title":"Matematicheskii Sbornik"},{"key":"446_CR18","doi-asserted-by":"publisher","unstructured":"Moura, L.M., Bj\u00f8rner, N.S.: Z3: an efficient SMT solver. In: Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference, TACAS\u201908. Lecture Notes in Computer Science, vol. 4963, pp. 337\u2013340. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"446_CR19","doi-asserted-by":"publisher","unstructured":"Oppen, D.C.: Elementary bounds for presburger arithmetic. In: Proceedings of the 5th Annual ACM Symposium on Theory of Computing, STOC\u201973, pp. 34\u201337. ACM, New York, NY, US (1973). https:\/\/doi.org\/10.1145\/800125.804033","DOI":"10.1145\/800125.804033"},{"key":"446_CR20","doi-asserted-by":"publisher","unstructured":"Plandowski, W.: Satisfiability of word equations with constants is in PSPACE. In: 40th Annual Symposium on Foundations of Computer Science, FOCS\u201999, pp. 495\u2013500. IEEE Computer Society, Washington, DC (1999). https:\/\/doi.org\/10.1109\/SFFCS.1999.814622","DOI":"10.1109\/SFFCS.1999.814622"},{"key":"446_CR21","unstructured":"Point, F.: On the expansion ($$\\mathbb{N}$$, $$+$$, $$2^x$$) of Presburger arithmetic. (2007). Unpublished. https:\/\/webusers.imj-prg.fr\/%7francoise.point\/papiers\/Pres.pdf"},{"key":"446_CR22","doi-asserted-by":"publisher","unstructured":"Saxena, P., Akhawe, D., Hanna, S., Mao, F., McCamant, S., Song, D.: A symbolic execution framework for javascript. In: 31st IEEE Symposium on Security and Privacy, S &P\u201910, pp. 513\u2013528. IEEE Computer Society, Washington, DC (2010). https:\/\/doi.org\/10.1109\/SP.2010.38","DOI":"10.1109\/SP.2010.38"},{"issue":"3","key":"446_CR23","doi-asserted-by":"publisher","first-page":"587","DOI":"10.1070\/IM1984v022n03ABEH001456","volume":"22","author":"AL Sem\u00ebnov","year":"1984","unstructured":"Sem\u00ebnov, A.L.: Logical theories of one-place functions on the set of natural numbers. Math. USSR-Izvestiya 22(3), 587\u2013618 (1984). https:\/\/doi.org\/10.1070\/IM1984v022n03ABEH001456","journal-title":"Math. USSR-Izvestiya"},{"key":"446_CR24","doi-asserted-by":"publisher","unstructured":"Trinh, M., Chu, D., Jaffar, J.: S3: A symbolic string solver for vulnerability detection in web applications. In: Ahn, G., Yung, M., Li, N. (eds.) Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, pp. 1232\u20131243. ACM, New York, NY, US (2014). https:\/\/doi.org\/10.1145\/2660267.2660372","DOI":"10.1145\/2660267.2660372"},{"key":"446_CR25","doi-asserted-by":"publisher","unstructured":"Yu, F., Alkhalaf, M., Bultan, T.: Stranger: An automata-based string analysis tool for PHP. In: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS\u201910. Lecture Notes in Computer Science, vol. 6015, pp. 154\u2013157. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_13","DOI":"10.1007\/978-3-642-12002-2_13"},{"key":"446_CR26","doi-asserted-by":"publisher","unstructured":"Zheng, Y., Zhang, X., Ganesh, V.: Z3-str: a z3-based string solver for web application analysis. In: Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, ESEC\/FSE\u201913, pp. 114\u2013124. ACM, New York, NY, USA (2013). https:\/\/doi.org\/10.1145\/2491411.2491456","DOI":"10.1145\/2491411.2491456"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-023-00446-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-023-00446-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-023-00446-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,2,21]],"date-time":"2024-02-21T19:02:50Z","timestamp":1708542170000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-023-00446-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,10,24]]},"references-count":26,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,3]]}},"alternative-id":["446"],"URL":"https:\/\/doi.org\/10.1007\/s00236-023-00446-4","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,10,24]]},"assertion":[{"value":"24 August 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 September 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"24 October 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}