{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,20]],"date-time":"2026-06-20T03:51:01Z","timestamp":1781927461051,"version":"3.54.5"},"publisher-location":"Cham","reference-count":14,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319242453","type":"print"},{"value":"9783319242460","type":"electronic"}],"license":[{"start":{"date-parts":[[2015,1,1]],"date-time":"2015-01-01T00:00:00Z","timestamp":1420070400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015]]},"DOI":"10.1007\/978-3-319-24246-0_8","type":"book-chapter","created":{"date-parts":[[2015,9,19]],"date-time":"2015-09-19T04:20:53Z","timestamp":1442636453000},"page":"119-134","source":"Crossref","is-referenced-by-count":13,"title":["Weakly Equivalent Arrays"],"prefix":"10.1007","author":[{"given":"J\u00fcrgen","family":"Christ","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Jochen","family":"Hoenicke","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2015,11,12]]},"reference":[{"key":"8_CR1","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Trans. Comput. Log.\u00a010(1) (2009)","DOI":"10.1145\/1459010.1459014"},{"key":"8_CR2","unstructured":"Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: 2.0. In: SMT (2010)"},{"issue":"1-3","key":"8_CR3","first-page":"165","volume":"6","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Lemmas on demand for the extensional theory of arrays. JSAT\u00a06(1-3), 165\u2013201 (2009)","journal-title":"JSAT"},{"key":"8_CR4","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-free interpolation of a theory of arrays. Logical Methods in Computer Science\u00a08(2) (2012)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"8_CR5","unstructured":"Christ, J., Hoenicke, J.: Weakly equivalent arrays. CoRR mabs\/1405.6939 (2014). http:\/\/arxiv.org\/abs\/1405.6939"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"248","DOI":"10.1007\/978-3-642-31759-0_19","volume-title":"Model Checking Software","author":"J. Christ","year":"2012","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: SMTInterpol: An interpolating SMT solver. In: Donaldson, A., Parker, D. (eds.) SPIN 2012. LNCS, vol.\u00a07385, pp. 248\u2013254. Springer, Heidelberg (2012)"},{"key":"8_CR7","doi-asserted-by":"crossref","unstructured":"Christ, J., Hoenicke, J., Nutz, A.: Proof tree preserving interpolation. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol.\u00a07795, pp. 124\u2013138. Springer, Heidelberg (2013)","DOI":"10.1007\/978-3-642-36742-7_9"},{"issue":"3","key":"8_CR8","doi-asserted-by":"publisher","first-page":"269","DOI":"10.2307\/2963594","volume":"22","author":"W. Craig","year":"1957","unstructured":"Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log.\u00a022(3), 269\u2013285 (1957)","journal-title":"J. Symb. Log."},{"key":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"key":"8_CR10","unstructured":"McCarthy, J.: Towards a mathematical science of computation. In: IFIP Congress, pp. 21\u201328 (1962)"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: FMCAD, pp. 45\u201352 (2009)","DOI":"10.1109\/FMCAD.2009.5351142"},{"key":"8_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1007\/978-3-540-32033-3_33","volume-title":"Term Rewriting and Applications","author":"R. Nieuwenhuis","year":"2005","unstructured":"Nieuwenhuis, R., Oliveras, A.: Proof-producing congruence closure. In: Giesl, J. (ed.) RTA 2005. LNCS, vol.\u00a03467, pp. 453\u2013468. Springer, Heidelberg (2005)"},{"key":"8_CR13","series-title":"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.\u00a03717, pp. 48\u201364. Springer, Heidelberg (2005)"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.R.: A decision procedure for an extensional theory of arrays. In: LICS, pp. 29\u201337. IEEE Computer Society (2001)","DOI":"10.1109\/LICS.2001.932480"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-24246-0_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,5,30]],"date-time":"2025-05-30T18:26:27Z","timestamp":1748629587000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-24246-0_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015]]},"ISBN":["9783319242453","9783319242460"],"references-count":14,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-24246-0_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015]]}}}