{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,20]],"date-time":"2026-09-20T04:43:31Z","timestamp":1789879411447,"version":"4.0.1"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2023,6,9]],"date-time":"2023-06-09T00:00:00Z","timestamp":1686268800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2023,10,31]]},"abstract":"<jats:p>In this article, we enrich McCarthy\u2019s theory of extensional arrays with a length and a maxdiff operation. As is well-known, some diff operation (i.e., some kind of difference function showing where two unequal arrays differ) is needed to keep interpolants quantifier free in array theories. Our maxdiff operation returns the max index where two arrays differ; thus, it has a univocally determined semantics.<\/jats:p>\n          <jats:p>The length function is a natural complement of such a maxdiff operation and is needed to handle real arrays. Obtaining interpolation results for such a rich theory is a surprisingly hard task. We get such results via a thorough semantic analysis of the models of the theory and of their amalgamation and strong amalgamation properties. The results are modular with respect to the index theory; we show how to convert them into concrete interpolation algorithms via a hierarchical approach realizing a polynomial reduction to interpolation in linear arithmetics endowed with free function symbols.<\/jats:p>","DOI":"10.1145\/3587161","type":"journal-article","created":{"date-parts":[[2023,3,13]],"date-time":"2023-03-13T12:30:08Z","timestamp":1678710608000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Interpolation Results for Arrays with Length and MaxDiff"],"prefix":"10.1145","volume":"24","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4216-5199","authenticated-orcid":false,"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[{"name":"Free University of Bozen-Bolzano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2464-2895","authenticated-orcid":false,"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[{"name":"University of New Mexico, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6779-2386","authenticated-orcid":false,"given":"Chiara","family":"Naso","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi di Milano, Italy"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,9]]},"reference":[{"key":"e_1_3_2_2_2","unstructured":"2021. AXDInterpolator. (2021). Retrieved December 10 2021 from https:\/\/github.com\/typesAreSpaces\/AXDInterpolator."},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-017-0279-6"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF02485230"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72013-1_24"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/11609773_28"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_28"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/2490253"},{"key":"e_1_3_2_10_2","unstructured":"Jos\u00e9 Abel Castellanos Joo Silvio Ghilardi Alessandro Gianola and Deepak Kapur. 2021. AXDInterpolator: A tool for computing interpolants for arrays with MaxDiff. In Proceedings of the 19th International Workshop on Satisfiability Modulo Theories (SMT\u201921) Vol. 2908. CEUR Workshop Proceedings 40\u201352. http:\/\/ceur-ws.org\/Vol-2908\/paper15.pdf."},{"key":"e_1_3_2_11_2","volume-title":"Model Theory (3rd ed.)","author":"Chang C. C.","year":"1990","unstructured":"C. C. Chang and H. Jerome Keisler. 1990. Model Theory (3rd ed.). North-Holland, Amsterdam-London."},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"J\u00fcrgen Christ Jochen Hoenicke and Alexander Nutz. 2012. SMTInterpol: An interpolating SMT solver. In Proceedings of the 19th International Workshop on Model Checking Software (SPIN\u201912) Alastair F. Donaldson and David Parker (Eds.). Vol. 7385. Springer Berlin 248\u2013254.","DOI":"10.1007\/978-3-642-31759-0_19"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36742-7_9"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.2307\/2963594"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71995-1_14"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-94205-6_36"},{"key":"e_1_3_2_19_2","article-title":"Interpolation and the array property fragment","volume":"1904","author":"Hoenicke Jochen","year":"2019","unstructured":"Jochen Hoenicke and Tanja Schindler. 2019. Interpolation and the array property fragment. CoRR abs\/1904.11381 (2019). arXiv:1904.11381http:\/\/arxiv.org\/abs\/1904.11381.","journal-title":"CoRR"},{"key":"e_1_3_2_20_2","doi-asserted-by":"crossref","unstructured":"Deepak Kapur Rupak Majumdar and Calogero G. Zarba. 2006. Interpolation for data structures. In Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering (FSE\u201906) . ACM 105\u2013116.","DOI":"10.1145\/1181775.1181789"},{"issue":"1","key":"e_1_3_2_21_2","first-page":"79","article-title":"Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity","volume":"18","author":"Kiss Emil W.","year":"1982","unstructured":"Emil W. Kiss, L\u00e1szl\u00f3 M\u00e1rki, P\u00e9ter Pr\u00f6hle, and Walter Tholen. 1982. Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Scientiarum Mathematicarum Hungarica 18, 1 (1982), 79\u2013140. SSMHAX","journal-title":"Studia Scientiarum Mathematicarum Hungarica"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25543-5_21"},{"key":"e_1_3_2_23_2","unstructured":"John McCarthy. 1962. Towards a mathematical science of computation. In Proceedings of the 2nd Congress on Information Processing (IFIP\u201962) . North-Holland 21\u201328."},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"e_1_3_2_25_2","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. 2006. Lazy abstraction with interpolants. In Proceedings of the 18th International Conference on Computer Aided Verification (CAV\u201906) Thomas Ball and Robert B. Jones (Eds.). Vol. 4144. Springer Berlin 123\u2013136.","DOI":"10.1007\/11817963_14"},{"key":"e_1_3_2_26_2","unstructured":"Kenneth L. McMillan. 2011. Interpolants from Z3 proofs. In Proceedings of the 11th International Conference on Formal Methods in Computer-Aided Design (FMCAD\u201911) . FMCAD Inc. 19\u201327."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-94583-1_15"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-69738-1_25"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.005"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_21"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(4:1)2008"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_19"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-14(3:23)2018"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429132"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9371-7"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_17"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587161","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3587161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:15Z","timestamp":1750178835000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3587161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,9]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2023,10,31]]}},"alternative-id":["10.1145\/3587161"],"URL":"https:\/\/doi.org\/10.1145\/3587161","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,9]]},"assertion":[{"value":"2022-04-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-01-24","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-06-09","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}