{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T06:45:59Z","timestamp":1770273959042,"version":"3.49.0"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783031107689","type":"print"},{"value":"9783031107696","type":"electronic"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_9","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"125-143","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Reasoning About Vectors Using an SMT Theory of Sequences"],"prefix":"10.1007","author":[{"given":"Ying","family":"Sheng","sequence":"first","affiliation":[]},{"given":"Andres","family":"N\u00f6tzli","sequence":"additional","affiliation":[]},{"given":"Andrew","family":"Reynolds","sequence":"additional","affiliation":[]},{"given":"Yoni","family":"Zohar","sequence":"additional","affiliation":[]},{"given":"David","family":"Dill","sequence":"additional","affiliation":[]},{"given":"Wolfgang","family":"Grieskamp","sequence":"additional","affiliation":[]},{"given":"Junkil","family":"Park","sequence":"additional","affiliation":[]},{"given":"Shaz","family":"Qadeer","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"issue":"3","key":"9_CR1","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1007\/s10703-017-0279-6","volume":"51","author":"F Alberti","year":"2017","unstructured":"Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51(3), 545\u2013574 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0279-6","journal-title":"Formal Methods Syst. Des."},{"key":"9_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H., et al.: cvc5: a versatile and industrial-strength SMT solver. In: Fisman, D., Rosu, G. (eds.) TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"key":"9_CR3","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The SMT-LIB Standard: Version 2.6. Technical report, Department of Computer Science, The University of Iowa (2017). www.SMT-LIB.org"},{"key":"9_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 512\u2013526. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11916277_35"},{"key":"9_CR5","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1007\/978-3-319-10575-8_11","volume-title":"Handbook of Model Checking","author":"C Barrett","year":"2018","unstructured":"Barrett, C., Tinelli, C.: Satisfiability modulo theories. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 305\u2013343. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11"},{"key":"9_CR6","doi-asserted-by":"crossref","unstructured":"Berzish, M., Ganesh, V., Zheng, Y.: Z3str3: a string solver with theory-aware heuristics. In: Stewart, D., Weissenbacher, G. (eds.) 2017 Formal Methods in Computer Aided Design, FMCAD 2017, Vienna, Austria, 2\u20136 October 2017, pp. 55\u201359. IEEE (2017)","DOI":"10.23919\/FMCAD.2017.8102241"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Bj\u00f8rner, N., de Moura, L., Nachmanson, L., Wintersteiger, C.: Programming Z3 (2018). https:\/\/theory.stanford.edu\/~nikolaj\/programmingz3.html#sec-sequences-and-strings","DOI":"10.1007\/978-3-030-17601-3_4"},{"key":"9_CR8","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":"9_CR9","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. 5505, pp. 307\u2013321. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-00768-2_27"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"119","DOI":"10.1007\/978-3-319-24246-0_8","volume-title":"Frontiers of Combining Systems","author":"J Christ","year":"2015","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. In: Lutz, C., Ranise, S. (eds.) FroCoS 2015. LNCS (LNAI), vol. 9322, pp. 119\u2013134. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-24246-0_8"},{"key":"9_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"9_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-030-81685-8_15","volume-title":"Computer Aided Verification","author":"N Elad","year":"2021","unstructured":"Elad, N., Rain, S., Immerman, N., Kov\u00e1cs, L., Sagiv, M.: Summing up smart transitions. In: Silva, A., Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 317\u2013340. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-81685-8_15"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic, 2nd edn. Academic Press (2001)","DOI":"10.1016\/B978-0-08-049646-7.50005-9"},{"key":"9_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-642-54108-7_6","volume-title":"Verified Software: Theories, Tools, Experiments","author":"S Falke","year":"2014","unstructured":"Falke, S., Merz, F., Sinz, C.: Extending the theory of arrays: memset, memcpy, and beyond. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 108\u2013128. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_6"},{"key":"9_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-39611-3_21","volume-title":"Hardware and Software: Verification and Testing","author":"V Ganesh","year":"2013","unstructured":"Ganesh, V., Minnes, M., Solar-Lezama, A., Rinard, M.: Word equations with length constraints: what\u2019s decidable? In: Biere, A., Nahir, A., Vos, T. (eds.) HVC 2012. LNCS, vol. 7857, pp. 209\u2013226. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39611-3_21"},{"key":"9_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR 2010. LNCS, vol. 6397, pp. 402\u2013416. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8_29"},{"key":"9_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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. 8559, pp. 646\u2013662. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_43"},{"issue":"2","key":"9_CR18","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson, G., Oppen, D.C.: Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1(2), 245\u2013257 (1979)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"9_CR19","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.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"9_CR20","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of Combining Systems","author":"S Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Zarba, C.G.: Combining data structures with nonstably infinite theories using many-sorted logic. In: Gramlich, B. (ed.) FroCoS 2005. LNCS (LNAI), vol. 3717, pp. 48\u201364. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11559306_3"},{"key":"9_CR21","unstructured":"Reynolds, A., N\u00f6tzli, A., Barrett, C.W., Tinelli, C.: Reductions for strings and regular expressions revisited. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21\u201324 September 2020, pp. 225\u2013235. IEEE (2020)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-319-63390-9_24","volume-title":"Computer Aided Verification","author":"A Reynolds","year":"2017","unstructured":"Reynolds, A., Woo, M., Barrett, C., Brumley, D., Liang, T., Tinelli, C.: Scaling up DPLL(T) string solvers using context-dependent simplification. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 453\u2013474. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_24"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Sheng, Y.,et al.: Reasoning about vectors using an SMT theory of sequences. CoRR 10.48550\/ARXIV.2205.08095 (2022)","DOI":"10.1007\/978-3-031-10769-6_9"},{"key":"9_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1007\/978-3-030-53288-8_7","volume-title":"Computer Aided Verification","author":"JE Zhong","year":"2020","unstructured":"Zhong, J.E., et al.: The move prover. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 137\u2013150. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53288-8_7"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,13]],"date-time":"2023-02-13T04:14:31Z","timestamp":1676261671000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"85","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"38% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5.2","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}