{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T19:27:48Z","timestamp":1790969268994,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540396253","type":"print"},{"value":"9783540396277","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1007\/11853886_16","type":"book-chapter","created":{"date-parts":[[2006,9,13]],"date-time":"2006-09-13T12:40:30Z","timestamp":1158151230000},"page":"177-189","source":"Crossref","is-referenced-by-count":4,"title":["Deciding Extensions of the Theory of Arrays by Integrating Decision Procedures and Instantiation Strategies"],"prefix":"10.1007","author":[{"given":"Silvio","family":"Ghilardi","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Enrica","family":"Nicolini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Daniele","family":"Zucchelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"16_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) FroCos 2005. LNCS, vol.\u00a03717, pp. 65\u201380. Springer, Heidelberg (2005)"},{"issue":"2","key":"16_CR2","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1016\/S0890-5401(03)00020-8","volume":"183","author":"A. Armando","year":"2003","unstructured":"Armando, A., Ranise, S., Rusinowitch, M.: A rewriting approach to satisfiability procedures. Information and Computation\u00a0183(2), 140\u2013164 (2003)","journal-title":"Information and Computation"},{"key":"16_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"427","DOI":"10.1007\/11609773_28","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2005","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 427\u2013442. Springer, Heidelberg (2005)"},{"issue":"4","key":"16_CR4","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1145\/322092.322104","volume":"25","author":"P.J. Downey","year":"1978","unstructured":"Downey, P.J., Sethi, R.: Assignment commands with array references. Journal of the ACM\u00a025(4), 652\u2013666 (1978)","journal-title":"Journal of the ACM"},{"key":"16_CR5","volume-title":"A Mathematical Introduction to Logic","author":"H.B. Enderton","year":"1972","unstructured":"Enderton, H.B.: A Mathematical Introduction to Logic. Academic Press, New York (1972)"},{"key":"16_CR6","volume-title":"Logic for Computer Science: Foundations of Automatic Theorem Proving","author":"J.H. Gallier","year":"1986","unstructured":"Gallier, J.H.: Logic for Computer Science: Foundations of Automatic Theorem Proving. Harper & Row, New York (1986)"},{"key":"16_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1007\/978-3-540-30124-0_9","volume-title":"Computer Science Logic","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Korovin, K.: Integrating equational reasoning into instantiation-based theorem proving. In: Marcinkowski, J., Tarlecki, A. (eds.) CSL 2004. LNCS, vol.\u00a03210, pp. 71\u201384. Springer, Heidelberg (2004)"},{"issue":"3-4","key":"16_CR8","doi-asserted-by":"publisher","first-page":"221","DOI":"10.1007\/s10817-004-6241-5","volume":"33","author":"S. Ghilardi","year":"2004","unstructured":"Ghilardi, S.: Model-theoretic methods in combined constraint satisfiability. Journal of Automated Reasoning\u00a033(3-4), 221\u2013249 (2004)","journal-title":"Journal of Automated Reasoning"},{"key":"16_CR9","unstructured":"Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Deciding extension of the theory of arrays by integrating decision procedures and instantiation strategies. Rapporto Interno DSI 309-06, Universit\u00e0 degli Studi di Milano, Milano, Italy (2006), Available at: \n                    \n                      http:\/\/homes.dsi.unimi.it\/~zucchell\/publications\/techreport\/GhiNiRaZu-RI309-06.pdf\n                    \n                    \n                  ."},{"issue":"2","key":"16_CR10","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/0020-0190(81)90007-7","volume":"12","author":"J. Jaffar","year":"1981","unstructured":"Jaffar, J.: Presburger arithmetic with array segments. Information Processing Letters\u00a012(2), 79\u201382 (1981)","journal-title":"Information Processing Letters"},{"key":"16_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"594","DOI":"10.1007\/11560647_39","volume-title":"Theoretical Aspects of Computing \u2013 ICTAC 2005","author":"H. Kirchner","year":"2005","unstructured":"Kirchner, H., Ranise, S., Ringeissen, C., Tran, D.-K.: On superposition-based satisfiability procedures and their combination. In: Van Hung, D., Wirsing, M. (eds.) ICTAC 2005. LNCS, vol.\u00a03722, pp. 594\u2013608. Springer, Heidelberg (2005)"},{"issue":"2","key":"16_CR12","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1145\/322248.322250","volume":"28","author":"P. Mateti","year":"1981","unstructured":"Mateti, P.: A decision procedure for the correctness of a class of programs. Journal of the ACM\u00a028(2), 215\u2013232 (1981)","journal-title":"Journal of the ACM"},{"key":"16_CR13","unstructured":"McCarthy, J.: Towards a mathematical theory of computation. In: Proceedings of IFIP Congress (1962)"},{"key":"16_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"476","DOI":"10.1007\/11513988_47","volume-title":"Computer Aided Verification","author":"S. McPeak","year":"2005","unstructured":"McPeak, S., Necula, G.C.: Data structure specifications via local equality axioms. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 476\u2013490. Springer, Heidelberg (2005)"},{"issue":"2","key":"16_CR15","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 Transaction on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transaction on Programming Languages and Systems"},{"key":"16_CR16","doi-asserted-by":"crossref","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning (2001)","DOI":"10.1016\/B978-044450813-3\/50009-6"},{"issue":"5","key":"16_CR17","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1145\/359104.359110","volume":"22","author":"J.C. Reynolds","year":"1979","unstructured":"Reynolds, J.C.: Reasoning about arrays. Communications of the ACM\u00a022(5), 290\u2013299 (1979)","journal-title":"Communications of the ACM"},{"key":"16_CR18","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures (2002)"},{"key":"16_CR19","volume-title":"Proc. of the 16th IEEE Symposium on Logic in Computer Science (LICS 2001)","author":"A. Stump","year":"2001","unstructured":"Stump, A., Barrett, C.W., Dill, D.L., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proc. of the 16th IEEE Symposium on Logic in Computer Science (LICS 2001). IEEE Computer Society, Los Alamitos (2001)"},{"issue":"1","key":"16_CR20","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/322169.322185","volume":"27","author":"N. Suzuki","year":"1980","unstructured":"Suzuki, N., Jefferson, D.R.: Verification decidability of presburger array programs. Journal of the ACM\u00a027(1), 191\u2013205 (1980)","journal-title":"Journal of the ACM"}],"container-title":["Lecture Notes in Computer Science","Logics in Artificial Intelligence"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11853886_16","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,11]],"date-time":"2019-03-11T02:50:24Z","timestamp":1552272624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11853886_16"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"ISBN":["9783540396253","9783540396277"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/11853886_16","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2006]]}}}