{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:05Z","timestamp":1751660525490,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030719944"},{"type":"electronic","value":"9783030719951"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,3,23]],"date-time":"2021-03-23T00:00:00Z","timestamp":1616457600000},"content-version":"vor","delay-in-days":81,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>In this paper, the theory of McCarthy\u2019s extensional arrays enriched with a maxdiff operation (this operation returns the biggest index where two given arrays differ) is proposed. It is known from the literature that a diff operation is required for the theory of arrays in order to enjoy the Craig interpolation property at the quantifier-free level. However, the diff operation introduced in the literature is merely instrumental to this purpose and has only a purely formal meaning (it is obtained from the Skolemization of the extensionality axiom). Our maxdiff operation significantly increases the level of expressivity; however, obtaining interpolation results for the resulting theory becomes a surprisingly hard task. We obtain such results via a thorough semantic analysis of the models of the theory and of their amalgamation properties. The results are modular with respect to the index theory and it is shown how to convert them into concrete interpolation algorithms via a hierarchical approach.<\/jats:p>","DOI":"10.1007\/978-3-030-71995-1_14","type":"book-chapter","created":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:03:39Z","timestamp":1616432619000},"page":"268-288","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Interpolation and Amalgamation for Arrays with MaxDiff"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-6449-6883","authenticated-orcid":false,"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4216-5199","authenticated-orcid":false,"given":"Alessandro","family":"Gianola","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2464-2895","authenticated-orcid":false,"given":"Deepak","family":"Kapur","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,3,23]]},"reference":[{"key":"14_CR1","unstructured":"AXDInterpolator, https:\/\/github.com\/typesAreSpaces\/AXDInterpolator, accessed: 2020-10-12"},{"key":"14_CR2","doi-asserted-by":"publisher","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: Lazy abstraction with interpolants for arrays. In: Proc. of LPAR-18. LNCS, vol.\u00a07180, pp. 46\u201361. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-28717-6_7","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"14_CR3","doi-asserted-by":"publisher","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: SAFARI: SMT-based abstraction for arrays with interpolants. In: Proc. of CAV. LNCS, vol.\u00a07358, pp. 679\u2013685. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_49","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"14_CR4","unstructured":"Alberti, F., Bruttomesso, R., Ghilardi, S., Ranise, S., Sharygina, N.: An extension of lazy abstraction with interpolation for programs with arrays. Formal Methods Syst. Des. 45(1), 63\u2013109 (2014)"},{"key":"14_CR5","doi-asserted-by":"publisher","unstructured":"Alberti, F., Ghilardi, S., Sharygina, N.: Booster: An acceleration-based verification framework for array programs. In: Proc. of ATVA. LNCS, vol.\u00a08837, pp. 18\u201323. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-11936-6_2","DOI":"10.1007\/978-3-319-11936-6_2"},{"key":"14_CR6","doi-asserted-by":"crossref","unstructured":"Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis 5, 45\u201355 (1975)","DOI":"10.1007\/BF02485230"},{"key":"14_CR7","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Proc. of VMCAI. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_28","DOI":"10.1007\/11609773_28"},{"key":"14_CR8","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Log. Methods Comput. Sci. 8(2) (2012)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"14_CR9","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation in combinations of equality interpolating theories. ACM Trans. Comput. Log. 15(1), 5:1\u20135:34 (2014)","DOI":"10.1145\/2490253"},{"key":"14_CR10","doi-asserted-by":"publisher","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, covers and superposition. In: Proc. of CADE. LNCS (LNAI), vol. 11716, pp. 142\u2013160. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_9","DOI":"10.1007\/978-3-030-29436-6_9"},{"key":"14_CR11","doi-asserted-by":"publisher","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Combined covers and Beth definability. In: Proc. of IJCAR. LNCS (LNAI), vol. 12166, pp. 181\u2013200. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_11","DOI":"10.1007\/978-3-030-51074-9_11"},{"key":"14_CR12","unstructured":"Calvanese, D., Ghilardi, S., Gianola, A., Montali, M., Rivkin, A.: Model completeness, uniform interpolants and superposition calculus (with applications to verificaton of data-aware processes). J. Autom. Reasoning (To appear)"},{"key":"14_CR13","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Gupta, A., Unadkat, D.: Verifying array manipulating programs with full-program induction. In: Proc. of TACAS. LNCS, vol. 12078, pp. 22\u201339. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-45190-5_2","DOI":"10.1007\/978-3-030-45190-5_2"},{"key":"14_CR14","unstructured":"Chang, C.C., Keisler, H.J.: Model Theory. North-Holland Publishing Co., Amsterdam-London, third edn. (1990)"},{"key":"14_CR15","doi-asserted-by":"crossref","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symbolic Logic 22, 269\u2013285 (1957)","DOI":"10.2307\/2963594"},{"key":"14_CR16","doi-asserted-by":"publisher","unstructured":"Fedyukovich, G., Prabhu, S., Madhukar, K., Gupta, A.: Quantified invariants via syntax-guided synthesis. In: Proc. of CAV. LNCS, vol. 11561, pp. 259\u2013277. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_14","DOI":"10.1007\/978-3-030-25540-4_14"},{"key":"14_CR17","doi-asserted-by":"crossref","unstructured":"Ghilardi, S.: Model theoretic methods in combined constraint satisfiability. J. Autom. Reasoning 33(3-4), 221\u2013249 (2004)","DOI":"10.1007\/s10817-004-6241-5"},{"key":"14_CR18","doi-asserted-by":"publisher","unstructured":"Ghilardi, S., Gianola, A.: Interpolation, amalgamation and combination (the non-disjoint signatures case). In: Proc. of FroCoS. LNCS (LNAI), vol. 10483, pp. 316\u2013332. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-66167-4_18","DOI":"10.1007\/978-3-319-66167-4_18"},{"key":"14_CR19","unstructured":"Ghilardi, S., Gianola, A.: Modularity results for interpolation, amalgamation and superamalgamation. Ann. Pure Appl. Logic 169(8), 731\u2013754 (2018)"},{"key":"14_CR20","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Computing uniform interpolants for EUF via (conditional) DAG-based compact representations. In: Proc. of CILC. CEUR Workshop Proceedings, vol.\u00a02710, pp. 67\u201381. CEUR-WS.org (2020)"},{"key":"14_CR21","unstructured":"Ghilardi, S., Gianola, A., Kapur, D.: Interpolation and amalgamation for Arrays with MaxDiff (extended version). Technical Report $${\\rm arXiv{:}2010.07082}$$, $${\\rm arXiv{.}org}$$ (2020), https:\/\/arxiv.org\/abs\/2010.07082"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Gurfinkel, A., Shoham, S., Vizel, Y.: Quantifiers on demand. In: Proc. of ATVA. LNCS, vol. 11138, pp. 248\u2013266. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_15","DOI":"10.1007\/978-3-030-01090-4_15"},{"key":"14_CR23","doi-asserted-by":"publisher","unstructured":"Hoenicke, J., Schindler, T.: Efficient interpolation for the theory of arrays. In: Proc. of IJCAR. LNCS (LNAI), vol. 10900, pp. 549\u2013565. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_36","DOI":"10.1007\/978-3-319-94205-6_36"},{"key":"14_CR24","doi-asserted-by":"publisher","unstructured":"Huang, G.: Constructing Craig interpolation formulas. In: Computing and Combinatorics COCOON. LNCS, vol.\u00a0959, pp. 181\u2013190. Springer (1995). https:\/\/doi.org\/10.1007\/BFb0030832","DOI":"10.1007\/BFb0030832"},{"key":"14_CR25","doi-asserted-by":"publisher","unstructured":"Ish-Shalom, O., Itzhaky, S., Rinetzky, N., Shoham, S.: Putting the squeeze on array programs: Loop verification via inductive rank reduction. In: Proc. of VMCAI. LNCS, vol. 11990, pp. 112\u2013135. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_6","DOI":"10.1007\/978-3-030-39322-9_6"},{"key":"14_CR26","unstructured":"Kapur, D.: Nonlinear polynomials, interpolants and invariant generation for system analysis. In: Proc. of the 2nd International Workshop on Satisfiability Checking and Symbolic Computation co-located with ISSAC (2017)"},{"key":"14_CR27","doi-asserted-by":"crossref","unstructured":"Kapur, D.: Conditional congruence closure over uninterpreted and interpreted symbols. J. Systems Science & Complexity 32(1), 317\u2013355 (2019)","DOI":"10.1007\/s11424-019-8377-8"},{"key":"14_CR28","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.G.: Interpolation for Data Structures. In: Proc. of SIGSOFT-FSE. pp. 105\u2013116. ACM (2006)","DOI":"10.1145\/1181775.1181789"},{"key":"14_CR29","doi-asserted-by":"publisher","unstructured":"Krishnan, H.G.V., Vizel, Y., Ganesh, V., Gurfinkel, A.: Interpolating strong induction. In: Proc. of CAV. LNCS, vol. 11562, pp. 367\u2013385. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-25543-5_21","DOI":"10.1007\/978-3-030-25543-5_21"},{"key":"14_CR30","unstructured":"McCarthy, J.: Towards a Mathematical Science of Computation. In: IFIP Congress. pp. 21\u201328 (1962)"},{"key":"14_CR31","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Proc. of CAV. LNCS, vol.\u00a02725, pp. 1\u201313. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45069-6_1","DOI":"10.1007\/978-3-540-45069-6_1"},{"key":"14_CR32","doi-asserted-by":"publisher","unstructured":"McMillan, K.L.: Lazy abstraction with interpolants. In: Proc. of CAV. LNCS, vol.\u00a04144, pp. 123\u2013136. Springer (2006). https:\/\/doi.org\/10.1007\/11817963_14","DOI":"10.1007\/11817963_14"},{"key":"14_CR33","doi-asserted-by":"crossref","unstructured":"Nelson, G., Oppen, D.C.: Simplification by Cooperating Decision Procedures. ACM Transactions on Programming Languages and Systems 1(2), 245\u201357 (1979)","DOI":"10.1145\/357073.357079"},{"key":"14_CR34","unstructured":"Pudl\u00e1k, P.: Lower bounds for resolution and cutting plane proofs and monotone computations. J. Symb. Log. 62(3), 981\u2013998 (1997)"},{"key":"14_CR35","doi-asserted-by":"crossref","unstructured":"Sofronie-Stokkermans, V.: Interpolation in local theory extensions. Log. Methods Comput. Sci. 4(4) (2008)","DOI":"10.2168\/LMCS-4(4:1)2008"},{"key":"14_CR36","unstructured":"Sofronie-Stokkermans, V.: On interpolation and symbol elimination in theory extensions. Log. Methods Comput. Sci. 14(3) (2018)"},{"key":"14_CR37","doi-asserted-by":"crossref","unstructured":"Totla, N., Wies, T.: Complete instantiation-based interpolation. J. Autom. Reasoning 57(1), 37\u201365 (2016)","DOI":"10.1007\/s10817-016-9371-7"},{"key":"14_CR38","doi-asserted-by":"publisher","unstructured":"Vizel, Y., Gurfinkel, A.: Interpolating property directed reachability. In: Proc. of CAV. LNCS, vol.\u00a08559, pp. 260\u2013276. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_17","DOI":"10.1007\/978-3-319-08867-9_17"}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-71995-1_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,3,22]],"date-time":"2021-03-22T17:06:30Z","timestamp":1616432790000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-71995-1_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030719944","9783030719951"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-71995-1_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"23 March 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FOSSACS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 March 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"1 April 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2021\/fossacs","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":"88","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":"28","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":"0","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":"32% - 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":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference changed to an online format due to the COVID-19 pandemic","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}