{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T14:29:13Z","timestamp":1725892153714},"publisher-location":"Berlin, Heidelberg","reference-count":32,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642313646"},{"type":"electronic","value":"9783642313653"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-31365-3_12","type":"book-chapter","created":{"date-parts":[[2012,6,21]],"date-time":"2012-06-21T16:35:34Z","timestamp":1340296534000},"page":"118-133","source":"Crossref","is-referenced-by-count":9,"title":["From Strong Amalgamability to Modularity of Quantifier-Free Interpolation"],"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":"12_CR1","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1007\/BF02485230","volume":"5","author":"P.D. Bacsich","year":"1975","unstructured":"Bacsich, P.D.: Amalgamation properties and interpolation theorems for equational theories. Algebra Universalis\u00a05, 45\u201355 (1975)","journal-title":"Algebra Universalis"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-540-70545-1_29","volume-title":"Computer Aided Verification","author":"D. Beyer","year":"2008","unstructured":"Beyer, D., Zufferey, D., Majumdar, R.: cSIsat: Interpolation for LA+EUF. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 304\u2013308. Springer, Heidelberg (2008)"},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/11513988_34","volume-title":"Computer Aided Verification","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Satisfiability Modulo Theories via Delayed Theory Combination. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 335\u2013349. Springer, Heidelberg (2005)"},{"key":"12_CR4","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":"12_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-18275-4_8","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A. Brillout","year":"2011","unstructured":"Brillout, A., Kroening, D., R\u00fcmmer, P., Wahl, T.: Beyond Quantifier-Free Interpolation in Extensions of Presburger Arithmetic. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 88\u2013102. Springer, Heidelberg (2011)"},{"key":"12_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-24364-6_8","volume-title":"Frontiers of Combining Systems","author":"R. Bruttomesso","year":"2011","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: A Combination of Rewriting and Constraint Solving for the Quantifier-Free Interpolation of Arrays with Integer Difference Constraints. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCos 2011. LNCS, vol.\u00a06989, pp. 103\u2013118. Springer, Heidelberg (2011)"},{"key":"12_CR7","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":"12_CR8","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: From Strong Amalgamation to Modularity of Quantifier-Free Interpolation. Technical Report RI 337-12, Dip. Scienze dell\u2019Informazione, Univ. di Milano (2012)","DOI":"10.1007\/978-3-642-31365-3_12"},{"key":"12_CR9","doi-asserted-by":"crossref","unstructured":"Bruttomesso, R., Ghilardi, S., Ranise, S.: Quantifier-Free Interpolation of a Theory of Arrays. Logical Methods in Computer Science (to appear, 2012)","DOI":"10.2168\/LMCS-8(2:4)2012"},{"key":"12_CR10","volume-title":"Model Theory","author":"C. Chang","year":"1990","unstructured":"Chang, C., Keisler, J.H.: Model Theory, 3rd edn. North-Holland, Amsterdam (1990)","edition":"3"},{"key":"12_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/978-3-540-78800-3_30","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Cimatti","year":"2008","unstructured":"Cimatti, A., Griggio, A., Sebastiani, R.: Efficient Interpolant Generation in Satisfiability Modulo Theories. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 397\u2013412. Springer, Heidelberg (2008)"},{"key":"12_CR12","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":"12_CR13","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)"},{"issue":"3-4","key":"12_CR14","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":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-642-02959-2_16","volume-title":"Automated Deduction \u2013 CADE-22","author":"A. Goel","year":"2009","unstructured":"Goel, A., Krsti\u0107, S., Tinelli, C.: Ground Interpolation for Combined Theories. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol.\u00a05663, pp. 183\u2013198. Springer, Heidelberg (2009)"},{"key":"12_CR16","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":"12_CR17","first-page":"729","volume":"3","author":"A.I. Mal\u2019cev","year":"1962","unstructured":"Mal\u2019cev, A.I.: Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. \u017d.\u00a03, 729\u2013743 (1962)","journal-title":"Sibirsk. Mat. \u017d."},{"key":"12_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"459","DOI":"10.1007\/11691372_33","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Jhala","year":"2006","unstructured":"Jhala, R., McMillan, K.L.: A Practical and Complete Approach to Predicate Refinement. In: Hermanns, H. (ed.) TACAS 2006. LNCS, vol.\u00a03920, pp. 459\u2013473. Springer, Heidelberg (2006)"},{"key":"12_CR19","doi-asserted-by":"crossref","first-page":"193","DOI":"10.7146\/math.scand.a-10468","volume":"4","author":"B. J\u00f3nsson","year":"1956","unstructured":"J\u00f3nsson, B.: Universal relational systems. Math. Scand.\u00a04, 193\u2013208 (1956)","journal-title":"Math. Scand."},{"key":"12_CR20","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":"12_CR21","first-page":"79","volume":"18","author":"E.W. Kiss","year":"1982","unstructured":"Kiss, E.W., M\u00e1rki, L., Pr\u00f6hle, P., Tholen, W.: Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Sci. Math. Hungar.\u00a018(1), 79\u2013140 (1982)","journal-title":"Studia Sci. Math. Hungar."},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"470","DOI":"10.1007\/978-3-642-00593-0_33","volume-title":"Fundamental Approaches to Software Engineering","author":"L. Kov\u00e1cs","year":"2009","unstructured":"Kov\u00e1cs, L., Voronkov, A.: Finding Loop Invariants for Programs over Arrays Using a Theorem Prover. In: Chechik, M., Wirsing, M. (eds.) FASE 2009. LNCS, vol.\u00a05503, pp. 470\u2013485. Springer, Heidelberg (2009)"},{"key":"12_CR23","unstructured":"McMillan, K.: Interpolants from Z3 proofs. In: Proc. of FMCAD (2011)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-24730-2_2","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.L. McMillan","year":"2004","unstructured":"McMillan, K.L.: An Interpolating Theorem Prover. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol.\u00a02988, pp. 16\u201330. Springer, Heidelberg (2004)"},{"issue":"1","key":"12_CR25","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":"12_CR26","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":"12_CR27","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1145\/322203.322204","volume":"27","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Reasoning about recursively defined data structures. Journal of the ACM\u00a027, 403\u2013411 (1980)","journal-title":"Journal of the ACM"},{"key":"12_CR28","doi-asserted-by":"publisher","first-page":"341","DOI":"10.1016\/0022-4049(72)90010-2","volume":"2","author":"C.M. Ringel","year":"1972","unstructured":"Ringel, C.M.: The intersection property of amalgamations. J. Pure Appl. Algebra\u00a02, 341\u2013342 (1972)","journal-title":"J. Pure Appl. Algebra"},{"issue":"11","key":"12_CR29","doi-asserted-by":"crossref","first-page":"1212","DOI":"10.1016\/j.jsc.2010.06.005","volume":"45","author":"A. Rybalchenko","year":"2010","unstructured":"Rybalchenko, A., Sofronie-Stokkermans, V.: Constraint Solving for Interpolation. J. of Symbolic Logic\u00a045(11), 1212\u20131233 (2010)","journal-title":"J. of Symbolic Logic"},{"key":"12_CR30","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/11814771_21","volume-title":"Automated Reasoning","author":"V. Sofronie-Stokkermans","year":"2006","unstructured":"Sofronie-Stokkermans, V.: Interpolation in Local Theory Extensions. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 235\u2013250. Springer, Heidelberg (2006)"},{"key":"12_CR31","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson-Oppen combination procedure. In: Proc. FroCoS 1996, pp. 103\u2013119 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"key":"12_CR32","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); Extended version available as Technical Report MSR-TR-2004-108, Microsoft Research (October 2004)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-31365-3_12.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T07:58:18Z","timestamp":1620115098000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-31365-3_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642313646","9783642313653"],"references-count":32,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-31365-3_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}