{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T10:04:51Z","timestamp":1743156291711,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642243639"},{"type":"electronic","value":"9783642243646"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-24364-6_8","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T01:22:21Z","timestamp":1317259341000},"page":"103-118","source":"Crossref","is-referenced-by-count":2,"title":["A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints"],"prefix":"10.1007","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"8_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"349","DOI":"10.1007\/3-540-61680-2_67","volume-title":"Algorithms - ESA 1996","author":"B. Cherkassky","year":"1996","unstructured":"Cherkassky, B., Goldberg, A.: Negative-cycle Detection Algorithms. In: D\u00edaz, J. (ed.) ESA 1996. LNCS, vol.\u00a01136, pp. 349\u2013363. Springer, Heidelberg (1996)"},{"key":"8_CR2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139172752","volume-title":"Term rewriting and all that","author":"F. Baader","year":"1998","unstructured":"Baader, F., Nipkow, T.: Term rewriting and all that. Cambridge University Press, Cambridge (1998)"},{"key":"8_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-642-14203-1_33","volume-title":"Automated Reasoning","author":"A. Brillout","year":"2010","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: An interpolating sequent calculus for quantifier-free presburger arithmetic. In: Giesl, J., H\u00e4hnle, R. (eds.) IJCAR 2010. LNCS, vol.\u00a06173, pp. 384\u2013399. Springer, Heidelberg (2010)"},{"key":"8_CR4","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In: VMCAI (to appear, 2012)"},{"key":"8_CR5","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. In: RTA (2011)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"8_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"150","DOI":"10.1007\/978-3-642-12002-2_12","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Bruttomesso","year":"2010","unstructured":"Bruttomesso, R., Pek, E., Sharygina, N., Tsitovich, A.: The openSMT solver. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol.\u00a06015, pp. 150\u2013153. Springer, Heidelberg (2010)"},{"key":"8_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1838552.1838559","volume":"12","author":"A. Cimatti","year":"2010","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolation Generation in Satisfiability Modulo Theories. ACM Trans. Comput. Logic\u00a012, 1\u201354 (2010)","journal-title":"ACM Trans. Comput. Logic"},{"key":"8_CR8","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":"8_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"413","DOI":"10.1007\/978-3-642-00768-2_34","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Fuchs","year":"2009","unstructured":"Fuchs, A., Goel, A., Grundy, J., Krsti\u0107, S., Tinelli, C.: Ground Interpolation for the Theory of Equality. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 413\u2013427. Springer, Heidelberg (2009)"},{"key":"8_CR10","doi-asserted-by":"crossref","unstructured":"Henzinger, T., McMillan, K.L., Jhala, R., Majumdar, R.: Abstractions from Proofs. In: POPL (2004)","DOI":"10.1145\/964001.964021"},{"key":"8_CR11","doi-asserted-by":"crossref","unstructured":"Kapur, D., Majumdar, R., Zarba, C.: Interpolation for Data Structures. In: SIGSOFT 2006\/FSE-14, pp. 105\u2013116 (2006)","DOI":"10.1145\/1181775.1181789"},{"issue":"1","key":"8_CR12","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.tcs.2005.07.003","volume":"345","author":"K.L. McMillan","year":"2005","unstructured":"McMillan, K.L.: An Interpolating Theorem Prover. Theor. Comput. Sci.\u00a0345(1), 101\u2013121 (2005)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"8_CR13","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 Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"8_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"346","DOI":"10.1007\/978-3-540-69738-1_25","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Rybalchenko","year":"2007","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol.\u00a04349, pp. 346\u2013362. Springer, Heidelberg (2007)"},{"key":"8_CR15","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"353","DOI":"10.1007\/11532231_26","volume-title":"Automated Deduction \u2013 CADE-20","author":"G. Yorsh","year":"2005","unstructured":"Yorsh, G., Musuvathi, M.: A Combination Method for Generating Interpolants. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol.\u00a03632, pp. 353\u2013368. Springer, Heidelberg (2005)"}],"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-642-24364-6_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T14:00:04Z","timestamp":1560693604000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24364-6_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243639","9783642243646"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24364-6_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}