{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:40:17Z","timestamp":1758566417132,"version":"3.44.0"},"reference-count":19,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T00:00:00Z","timestamp":1755734400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T00:00:00Z","timestamp":1755734400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100007241","name":"Universit\u00e9 Paris-Saclay","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100007241","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2025,9]]},"abstract":"<jats:title>Abstract<\/jats:title>\n          <jats:p>The SMT (Satisfiability Modulo Theories) theory of arrays is well-established and widely used, with various decision procedures and extensions developed for it. However, recent contributions suggest that developing tailored reasoning for some theories, such as sequences and strings, can be more efficient than reasoning over them through axiomatization over the theory of arrays. In this paper, we are interested in reasoning over <jats:inline-formula>\n              <jats:tex-math>$$n$$<\/jats:tex-math>\n            <\/jats:inline-formula>-indexed sequences as they are found in some programming languages, such as Ada. We propose an SMT theory of <jats:inline-formula>\n              <jats:tex-math>$$n$$<\/jats:tex-math>\n            <\/jats:inline-formula>-indexed sequences and explore different ways to represent and reason over <jats:inline-formula>\n              <jats:tex-math>$$n$$<\/jats:tex-math>\n            <\/jats:inline-formula>-indexed sequences using existing theories, as well as tailored calculi for this theory.<\/jats:p>","DOI":"10.1007\/s00236-025-00496-w","type":"journal-article","created":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T04:47:17Z","timestamp":1755751637000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Reasoning over n-indexed sequences in SMT"],"prefix":"10.1007","volume":"62","author":[{"given":"Hichem Rami","family":"Ait-El-Hara","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fran\u00e7ois","family":"Bobot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillaume","family":"Bury","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,21]]},"reference":[{"key":"496_CR1","unstructured":"Ait-El-Hara, H.R., Bobot, F., Bury, G.: An SMT Theory for n-Indexed Sequences. In: Reger, G., Zohar, Y. (eds.) Proceedings of the 22nd International Workshop on Satisfiability Modulo Theories. CEUR Workshop Proceedings, vol. 3725, pp. 64\u201374. CEUR, Montreal, Canada (2024). https:\/\/ceur-ws.org\/Vol-3725\/#short13"},{"key":"496_CR2","doi-asserted-by":"publisher","unstructured":"Ait-El-Hara, H.R., Bobot, F., Bury, G.: On SMT Theory Design: The Case of Sequences. In: Kalpa Publications in Computing, vol. 18, pp. 14\u201329. EasyChair, Balaclava, Mauritius (2024). https:\/\/doi.org\/10.29007\/75tl. ISSN: 2515-1762","DOI":"10.29007\/75tl"},{"key":"496_CR3","doi-asserted-by":"publisher","unstructured":"Barbosa, H., Barrett, C.W., Brain, M., Kremer, G., Lachnitt, H., Mann, M., Mohamed, A., Mohamed, M., Niemetz, A., N\u00f6tzli, A., Ozdemir, A., Preiner, M., Reynolds, A., Sheng, Y., Tinelli, C., Zohar, Y.: cvc5: A versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 415\u2013442. Springer, Munich, Germany (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"496_CR4","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK) (2010)"},{"key":"496_CR5","doi-asserted-by":"crossref","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: Proceedings of the 17th Conference on Formal Methods in Computer-Aided Design. FMCAD \u201917, pp. 55\u201359. FMCAD Inc, Austin, Texas (2017)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"496_CR6","unstructured":"Bj\u00f8rner, N., Ganesh, V., Michel, R., Veanes, M.: An SMT-LIB Format for Sequences and Regular Expressions. Strings (2012)"},{"key":"496_CR7","unstructured":"Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: CDSAT for Nondisjoint Theories with Shared Predicates: Arrays With Abstract Length. Satisfiability Modulo Theories workshop, CEUR Workshop Proceedings 3185 (2022). Accessed 2024-02-23"},{"key":"496_CR8","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s Decidable About Arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 427\u2013442. Springer, Berlin, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11609773_28","DOI":"10.1007\/11609773_28"},{"key":"496_CR9","doi-asserted-by":"publisher","unstructured":"Christ, J., Hoenicke, J.: Weakly Equivalent Arrays. In: Lutz, C., Ranise, S. (eds.) Frontiers of Combining Systems. Lecture Notes in Computer Science, pp. 119\u2013134. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_8","DOI":"10.1007\/978-3-319-24246-0_8"},{"key":"496_CR10","doi-asserted-by":"publisher","unstructured":"Furia, C.A.: What\u2019s Decidable about Sequences? In: Bouajjani, A., Chin, W.-N. (eds.) Automated Technology for Verification and Analysis, pp. 128\u2013142. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-15643-4_11","DOI":"10.1007\/978-3-642-15643-4_11"},{"issue":"4","key":"496_CR11","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1145\/3587161","volume":"24","author":"S Ghilardi","year":"2023","unstructured":"Ghilardi, S., Gianola, A., Kapur, D., Naso, C.: Interpolation Results for Arrays with Length and MaxDiff. ACM Trans. Comput. Log. 24(4), 28\u201312833 (2023). https:\/\/doi.org\/10.1145\/3587161","journal-title":"ACM Trans. Comput. Log."},{"key":"496_CR12","doi-asserted-by":"publisher","unstructured":"Je\u017c, A., Lin, A.W., Markgraf, O., R\u00fcmmer, P.: Decision Procedures for\u00a0Sequence Theories. In: Enea, C., Lal, A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, pp. 18\u201340. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-37703-7_2","DOI":"10.1007\/978-3-031-37703-7_2"},{"key":"496_CR13","doi-asserted-by":"publisher","unstructured":"Lesbre, D., Lemerre, M., Ait-El-Hara, H.R., Bobot, F.: Relational abstractions based on labeled union-find. Proc. ACM Program. Lang. 9(PLDI) (2025). https:\/\/doi.org\/10.1145\/3729298","DOI":"10.1145\/3729298"},{"key":"496_CR14","doi-asserted-by":"publisher","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.) Computer Aided Verification, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43","DOI":"10.1007\/978-3-319-08867-9_43"},{"key":"496_CR15","unstructured":"Marre, B., Bobot, F., Chihani, Z.: Real Behavior of Floating Point Numbers. In: The SMT Workshop, Heidelberg, Germany (2017). SMT 2017, 15th International Workshop on Satisfiability Modulo Theories. https:\/\/cea.hal.science\/cea-01795760"},{"key":"496_CR16","doi-asserted-by":"publisher","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: An efficient smt solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 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"},{"issue":"3","key":"496_CR17","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/s10817-023-09682-2","volume":"67","author":"Y Sheng","year":"2023","unstructured":"Sheng, Y., N\u00f6tzli, A., Reynolds, A., Zohar, Y., Dill, D., Grieskamp, W., Park, J., Qadeer, S., Barrett, C., Tinelli, C.: Reasoning About Vectors: Satisfiability Modulo a Theory of Sequences. J. Autom. Reason. 67(3), 32 (2023). https:\/\/doi.org\/10.1007\/s10817-023-09682-2","journal-title":"J. Autom. Reason."},{"key":"496_CR18","doi-asserted-by":"publisher","unstructured":"Varghese, G., Lauck, T.: Hashed and hierarchical timing wheels: Data structures for the efficient implementation of a timer facility. In: Proceedings of the Eleventh ACM Symposium on Operating Systems Principles, vol. 21, pp. 25\u201338. Association for Computing Machinery, New York, NY, USA (1987). https:\/\/doi.org\/10.1145\/37499.37504","DOI":"10.1145\/37499.37504"},{"issue":"1","key":"496_CR19","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10817-022-09654-y","volume":"67","author":"Q Wang","year":"2023","unstructured":"Wang, Q., Appel, A.W.: A Solver for Arrays with Concatenation. J. Autom. Reason. 67(1), 4 (2023). https:\/\/doi.org\/10.1007\/s10817-022-09654-y","journal-title":"J. Autom. Reason."}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00496-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00236-025-00496-w\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-025-00496-w.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,22]],"date-time":"2025-09-22T18:02:44Z","timestamp":1758564164000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00236-025-00496-w"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,21]]},"references-count":19,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["496"],"URL":"https:\/\/doi.org\/10.1007\/s00236-025-00496-w","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"type":"print","value":"0001-5903"},{"type":"electronic","value":"1432-0525"}],"subject":[],"published":{"date-parts":[[2025,8,21]]},"assertion":[{"value":"2 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"4 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"33"}}