{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T12:57:22Z","timestamp":1758632242235,"version":"3.37.3"},"reference-count":25,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T00:00:00Z","timestamp":1673049600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T00:00:00Z","timestamp":1673049600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-1521602"],"award-info":[{"award-number":["CCF-1521602"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR001120C0160"],"award-info":[{"award-number":["HR001120C0160"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2023,3]]},"DOI":"10.1007\/s10817-022-09654-y","type":"journal-article","created":{"date-parts":[[2023,1,7]],"date-time":"2023-01-07T15:24:28Z","timestamp":1673105068000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["A Solver for Arrays with Concatenation"],"prefix":"10.1007","volume":"67","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-6486-3409","authenticated-orcid":false,"given":"Qinshi","family":"Wang","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-6009-0325","authenticated-orcid":false,"given":"Andrew W.","family":"Appel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,7]]},"reference":[{"key":"9654_CR1","doi-asserted-by":"publisher","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: International Conference on Computer Aided Verification, pp.\u00a0150\u2013166. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_10","DOI":"10.1007\/978-3-319-08867-9_10"},{"key":"9654_CR2","doi-asserted-by":"publisher","unstructured":"Abdulla, P.A., Atig, M.F., Diep, B.P., Hol\u00edk, L., Jank\u016f, P.: Chain-free string constraints. In: International Symposium on Automated Technology for Verification and Analysis, pp.\u00a0277\u2013293. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_16","DOI":"10.1007\/978-3-030-31784-3_16"},{"key":"9654_CR3","doi-asserted-by":"publisher","unstructured":"Appel, A.W.: Verified software toolchain. In: European Symposium on Programming, pp.\u00a01\u201317. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-19718-5_1","DOI":"10.1007\/978-3-642-19718-5_1"},{"key":"9654_CR4","doi-asserted-by":"publisher","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Handbook of Model Checking, pp.\u00a0305\u2013343. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"key":"9654_CR5","doi-asserted-by":"publisher","unstructured":"Besson, F., Cornilleau, P.-E., Pichardie, D.: Modular SMT proofs for fast reflexive checking inside coq. In: International Conference on Certified Programs and Proofs, pp.\u00a0151\u2013166. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-25379-9_13","DOI":"10.1007\/978-3-642-25379-9_13"},{"key":"9654_CR6","first-page":"76","volume":"12","author":"N Bj\u00f8rner","year":"2012","unstructured":"Bj\u00f8rner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB format for sequences and regular expressions. SMT 12, 76\u201386 (2012)","journal-title":"SMT"},{"key":"9654_CR7","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma,H.B.: What\u2019s decidable about arrays? In: International Workshop on Verification, Model Checking, and Abstract Interpretation, pp.\u00a0427\u2013442. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_28","DOI":"10.1007\/11609773_28"},{"issue":"1\u20134","key":"9654_CR8","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10817-018-9457-5","volume":"61","author":"Q Cao","year":"2018","unstructured":"Cao, Q., Beringer, L., Gruetter, S., Dodds, J., Appel, A.W.: VST-Floyd: a separation logic tool to verify correctness of C programs. J. Autom. Reason. 61(1\u20134), 367\u2013422 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9457-5","journal-title":"J. Autom. Reason."},{"key":"9654_CR9","doi-asserted-by":"publisher","unstructured":"Chen, T., Chen, Y., Hague, M., Lin, A.W., Wu, Z..: What is decidable about string constraints with the replaceall function. In: Proceedings of the ACM on Programming Languages, 2(POPL):1\u201329 (2017). https:\/\/doi.org\/10.1145\/3158091","DOI":"10.1145\/3158091"},{"key":"9654_CR10","doi-asserted-by":"publisher","unstructured":"Daca, P., Henzinger, T.A., Kupriyanov, A.: Array folds logic. In: International Conference on Computer Aided Verification, pp.\u00a0230\u2013248. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_13","DOI":"10.1007\/978-3-319-41540-6_13"},{"key":"9654_CR11","doi-asserted-by":"publisher","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Haifa Verification Conference, pp.\u00a0209\u2013226. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21","DOI":"10.1007\/978-3-642-39611-3_21"},{"key":"9654_CR12","doi-asserted-by":"publisher","unstructured":"Ge, Y., De Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: International Conference on Computer Aided Verification, pp.\u00a0306\u2013320. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_25","DOI":"10.1007\/978-3-642-02658-4_25"},{"key":"9654_CR13","doi-asserted-by":"publisher","unstructured":"Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: International Conference on Foundations of Software Science and Computational Structures, pp.\u00a0474\u2013489. Springer (2008). https:\/\/doi.org\/10.1007\/978-3-540-78499-9_33","DOI":"10.1007\/978-3-540-78499-9_33"},{"key":"9654_CR14","doi-asserted-by":"publisher","unstructured":"Hol\u00edk, L., Jank\u016f, 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), pp.\u00a01\u201332 (2017). https:\/\/doi.org\/10.1145\/3158092","DOI":"10.1145\/3158092"},{"key":"9654_CR15","doi-asserted-by":"publisher","unstructured":"Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: Verifast: A powerful, sound, predictable, fast verifier for C and Java. In: NASA Formal Methods Symposium, pp.\u00a041\u201355. Springer (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_4","DOI":"10.1007\/978-3-642-20398-5_4"},{"key":"9654_CR16","doi-asserted-by":"publisher","unstructured":"Leino, K., Rustan, M.: Dafny: An automatic program verifier for functional correctness. In: International Conference on Logic for Programming Artificial Intelligence and Reasoning, pp.\u00a0348\u2013370. Springer (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_20","DOI":"10.1007\/978-3-642-17511-4_20"},{"key":"9654_CR17","doi-asserted-by":"publisher","unstructured":"Lin, A.W., Barcel\u00f3, P.: String solving with word equations and transducers: towards a logic for analysing mutation XSS. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.\u00a0123\u2013136 (2016). https:\/\/doi.org\/10.1145\/2837614.2837641","DOI":"10.1145\/2837614.2837641"},{"key":"9654_CR18","doi-asserted-by":"crossref","unstructured":"Makanin, G.S.: The problem of solvability of equations in a free semigroup. Matematicheskii Sbornik 145(2), 147\u2013236 (1977)","DOI":"10.1070\/SM1977v032n02ABEH002376"},{"key":"9654_CR19","doi-asserted-by":"publisher","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: Program Verification, pp.\u00a035\u201356. Springer (1993). https:\/\/doi.org\/10.1007\/978-94-011-1793-7_2","DOI":"10.1007\/978-94-011-1793-7_2"},{"key":"9654_CR20","volume-title":"Computation: Finite and Infinite Machines","author":"ML Minsky","year":"1967","unstructured":"Minsky, M.L.: Computation: Finite and Infinite Machines. Prentice-Hall Inc, Hoboken (1967)"},{"issue":"3","key":"9654_CR21","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 51(3), 483\u2013496 (2004). https:\/\/doi.org\/10.1145\/990308.990312","journal-title":"J. ACM"},{"key":"9654_CR22","doi-asserted-by":"publisher","unstructured":"Plandowski, W.: An efficient algorithm for solving word equations. In: Proceedings of the Thirty-Eighth Annual ACM Symposium on Theory of Computing, pp.\u00a0467\u2013476. ACM (2006). https:\/\/doi.org\/10.1145\/1132516.1132584","DOI":"10.1145\/1132516.1132584"},{"key":"9654_CR23","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.\u00a029\u201337. IEEE (2001)","DOI":"10.1109\/LICS.2001.932480"},{"key":"9654_CR24","doi-asserted-by":"crossref","unstructured":"Zaostrovnykh, A., Pirelli, S., Pedrosa, L., Argyraki, K., Candea, G.: A formally verified NAT. In: Proceedings of the Conference of the ACM Special Interest Group on Data Communication (SIGCOMM\u201917), pp.\u00a0141\u2013154 (2017)","DOI":"10.1145\/3098822.3098833"},{"issue":"2\u20133","key":"9654_CR25","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1007\/s10703-016-0263-6","volume":"50","author":"Y Zheng","year":"2017","unstructured":"Zheng, Y., Ganesh, V., Subramanian, S., Tripp, O., Berzish, M., Dolby, J., Zhang, X.: Z3str2: an efficient solver for strings, regular expressions, and length constraints. Formal Methods System Des 50(2\u20133), 249\u2013288 (2017). https:\/\/doi.org\/10.1007\/s10703-016-0263-6","journal-title":"Formal Methods System Des"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09654-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-022-09654-y\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-022-09654-y.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,11]],"date-time":"2024-10-11T20:22:06Z","timestamp":1728678126000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-022-09654-y"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,7]]},"references-count":25,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2023,3]]}},"alternative-id":["9654"],"URL":"https:\/\/doi.org\/10.1007\/s10817-022-09654-y","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2023,1,7]]},"assertion":[{"value":"6 May 2021","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"5 October 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"There are no conflicts of interest. Code is available open-source as described in the paper.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of interest"}}],"article-number":"4"}}