{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,15]],"date-time":"2026-05-15T01:29:18Z","timestamp":1778808558157,"version":"3.51.4"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2014,2,1]],"date-time":"2014-02-01T00:00:00Z","timestamp":1391212800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"PRIN 2010-2011 project Logical Methods for Information Management"},{"name":"Italian Ministry of Education, University and Research (MIUR)"},{"name":"Automated Security Analysis of Identity and Access Management Systems (SIAM) project"},{"name":"Provincia Autonoma di Trento in the context of the &#8220;team 2009 - Incoming&#8221; COFUND action of the European Commission (FP7)"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2014,2]]},"abstract":"<jats:p>\n            The use of interpolants in verification is gaining more and more importance. Since theories used in applications are usually obtained as (disjoint) combinations of simpler theories, it is important to modularly reuse interpolation algorithms for the component theories. We show that a sufficient and necessary condition to do this for quantifier-free interpolation is that the component theories have the\n            <jats:italic>strong<\/jats:italic>\n            (\n            <jats:italic>sub<\/jats:italic>\n            -)\n            <jats:italic>amalgamation<\/jats:italic>\n            property. Then, we provide an equivalent syntactic characterization and show that such characterization covers most theories commonly employed in verification. Finally, we design a combined quantifier-free interpolation algorithm capable of handling both convex and nonconvex theories; this algorithm subsumes and extends most existing work on combined interpolation.\n          <\/jats:p>","DOI":"10.1145\/2490253","type":"journal-article","created":{"date-parts":[[2014,3,4]],"date-time":"2014-03-04T13:24:59Z","timestamp":1393939499000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":20,"title":["Quantifier-free interpolation in combinations of equality interpolating theories"],"prefix":"10.1145","volume":"15","author":[{"given":"Roberto","family":"Bruttomesso","sequence":"first","affiliation":[{"name":"Universit\u00e0 degli Studi, Milano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ghilardi","sequence":"additional","affiliation":[{"name":"Universit\u00e0 degli Studi, Milano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,3,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-28717-6_7"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_49"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02485230"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_29"},{"key":"e_1_2_1_5_1","volume-title":"Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'11)","volume":"6793","author":"Bonacina M. P.","unstructured":"M. P. Bonacina and M. Johansson . 2011. On interpolation in decision procedures . In Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'11) . Lecture Notes in Computer Science , Vol. 6793 , Springer-Verlag, Berlin, 1--16. M. P. Bonacina and M. Johansson. 2011. On interpolation in decision procedures. In Proceedings of the 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX'11). Lecture Notes in Computer Science, Vol. 6793, Springer-Verlag, Berlin, 1--16."},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/11513988_34"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-1_33"},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11)","volume":"5538","author":"Brillout A.","unstructured":"A. Brillout , D. Kroening , P. R\u00fcmmer , and T. Wahl . 2011. Beyond quantifier-free interpolation in extensions of Presburger arithmetic . In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11) . Lecture Notes in Computer Science , Vol. 5538 , Springer-Verlag, Berlin, 88--102. A. Brillout, D. Kroening, P. R\u00fcmmer, and T. Wahl. 2011. Beyond quantifier-free interpolation in extensions of Presburger arithmetic. In Proceedings of the 12th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI'11). Lecture Notes in Computer Science, Vol. 5538, Springer-Verlag, Berlin, 88--102."},{"key":"e_1_2_1_9_1","volume-title":"Proceedings of the 8th International Symposium on Frontiers of Combining System (FroCoS'11)","volume":"6989","author":"Bruttomesso R.","unstructured":"R. Bruttomesso , S. Ghilardi , and S. Ranise . 2011a. A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints . In Proceedings of the 8th International Symposium on Frontiers of Combining System (FroCoS'11) . Lecture Notes in Computer Science , Vol. 6989 , Springer-Verlag, Berlin, 103--118. R. Bruttomesso, S. Ghilardi, and S. Ranise. 2011a. A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints. In Proceedings of the 8th International Symposium on Frontiers of Combining System (FroCoS'11). Lecture Notes in Computer Science, Vol. 6989, Springer-Verlag, Berlin, 103--118."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA'11)","author":"Bruttomesso R.","unstructured":"R. Bruttomesso , S. Ghilardi , and S. Ranise . 2011b. Rewriting-based quantifier-free interpolation for a theory of arrays . In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA'11) . Dagstuhl Publishing, 171--186. R. Bruttomesso, S. Ghilardi, and S. Ranise. 2011b. Rewriting-based quantifier-free interpolation for a theory of arrays. In Proceedings of the 22th International Conference on Rewriting Techniques and Applications (RTA'11). Dagstuhl Publishing, 171--186."},{"key":"e_1_2_1_11_1","first-page":"2","article-title":"Quantifier-free interpolation for a theory of arrays","volume":"8","author":"Bruttomesso R.","year":"2012","unstructured":"R. Bruttomesso , S. Ghilardi , and S. Ranise . 2012 . Quantifier-free interpolation for a theory of arrays . Logic. Methods Comput. Science 8 , 2 . R. Bruttomesso, S. Ghilardi, and S. Ranise. 2012. Quantifier-free interpolation for a theory of arrays. Logic. Methods Comput. Science 8, 2.","journal-title":"Logic. Methods Comput. Science"},{"key":"e_1_2_1_12_1","unstructured":"C. Chang and J. H. Keisler. 1990. Model Theory 3rd Ed. North-Holland Amsterdam-London.  C. Chang and J. H. Keisler. 1990. Model Theory 3rd Ed. North-Holland Amsterdam-London."},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of System (TACAS'08)","volume":"4963","author":"Cimatti A.","unstructured":"A. Cimatti , A. Griggio , and R. Sebastiani . 2008. Efficient interpolant generation in satisfiability modulo theories . In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of System (TACAS'08) . Lecture Notes in Computer Science , Vol. 4963 , Springer-Verlag, Berlin, 397--412. A. Cimatti, A. Griggio, and R. Sebastiani. 2008. Efficient interpolant generation in satisfiability modulo theories. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of System (TACAS'08). Lecture Notes in Computer Science, Vol. 4963, Springer-Verlag, Berlin, 397--412."},{"key":"e_1_2_1_14_1","doi-asserted-by":"crossref","unstructured":"W. Craig. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 269--285.  W. Craig. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. J. Symb. Log. 269--285.","DOI":"10.2307\/2963594"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/0097-3165(73)90004-6"},{"key":"e_1_2_1_16_1","unstructured":"L. van den Dries. 2010. Mathematical logic lecture notes. Tech. rep. http:\/\/www.math.uiuc.edu\/&sim;vddries\/main.pdf.  L. van den Dries. 2010. Mathematical logic lecture notes. Tech. rep. http:\/\/www.math.uiuc.edu\/&sim;vddries\/main.pdf."},{"key":"e_1_2_1_17_1","volume-title":"A Mathematical Introduction to Logic","author":"Enderton Herbert B.","unstructured":"Herbert B. Enderton . 1972. A Mathematical Introduction to Logic . Academic Press , New York-London. Herbert B. Enderton. 1972. A Mathematical Introduction to Logic. Academic Press, New York-London."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00768-2_34"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-004-6241-5"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_16"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964021"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_33"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.7146\/math.scand.a-10468"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1181775.1181789"},{"key":"e_1_2_1_25_1","first-page":"79","article-title":"Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Sci","volume":"18","author":"Kiss E. W.","year":"1982","unstructured":"E. W. Kiss , L. M\u00e1rki , P. Pr\u00f6hle , and W. Tholen . 1982 . Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Sci . Math. Hungar. 18 , 1, 79 -- 140 . E. W. Kiss, L. M\u00e1rki, P. Pr\u00f6hle, and W. Tholen. 1982. Categorical algebraic properties. A compendium on amalgamation, congruence extension, epimorphisms, residual smallness, and injectivity. Studia Sci. Math. Hungar. 18, 1, 79--140.","journal-title":"Math. Hungar."},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00593-0_33"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02959-2_17"},{"key":"e_1_2_1_28_1","unstructured":"A. I. Mal'cev. 1962. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. \u017d. 3 729--743.  A. I. Mal'cev. 1962. Axiomatizable classes of locally free algebras of certain types. Sibirsk. Mat. \u017d. 3 729--743."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_2"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.003"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/11494744_2"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/2157654.2157661"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/357073.357079"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/322203.322204"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(72)90010-2"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jsc.2010.06.005"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_21"},{"key":"e_1_2_1_38_1","volume-title":"Proceedings of the 1st International Workshop on Frontiers of Combining System (FroCos'96)","volume":"3","author":"Tinelli C.","unstructured":"C. Tinelli and M. T. Harandi . 1996. A new correctness proof of the Nelson-Oppen combination procedure . In Proceedings of the 1st International Workshop on Frontiers of Combining System (FroCos'96) . Applied Logic , Vol. 3 , Springer Science&plus;Business Media B. V., The Netherlands, 103--119. C. Tinelli and M. T. Harandi. 1996. A new correctness proof of the Nelson-Oppen combination procedure. In Proceedings of the 1st International Workshop on Frontiers of Combining System (FroCos'96). Applied Logic, Vol. 3, Springer Science&plus;Business Media B. V., The Netherlands, 103--119."},{"key":"e_1_2_1_39_1","volume-title":"Tech. Rep. MSR-TR-2004-108.","author":"Yorsh G.","year":"2004","unstructured":"G. Yorsh and M. Musuvathi . 2004 . A combination method for generating interpolants. Tech. Rep. MSR-TR-2004-108. G. Yorsh and M. Musuvathi. 2004. A combination method for generating interpolants. Tech. Rep. MSR-TR-2004-108."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_26"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2490253","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2490253","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:34:33Z","timestamp":1750232073000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2490253"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,2]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2014,2]]}},"alternative-id":["10.1145\/2490253"],"URL":"https:\/\/doi.org\/10.1145\/2490253","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,2]]},"assertion":[{"value":"2012-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-03-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}