{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T07:40:31Z","timestamp":1743147631377,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":21,"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_14","type":"book-chapter","created":{"date-parts":[[2011,9,29]],"date-time":"2011-09-29T01:22:21Z","timestamp":1317259341000},"page":"195-210","source":"Crossref","is-referenced-by-count":6,"title":["Sharing Is Caring: Combination of Theories"],"prefix":"10.1007","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"14_CR1","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C.W. Barrett","year":"2006","unstructured":"Barrett, C.W., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on Demand in SAT Modulo Theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, pp. 512\u2013526. Springer, Heidelberg (2006)"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 298\u2013302. Springer, Heidelberg (2007)"},{"issue":"10","key":"14_CR3","doi-asserted-by":"publisher","first-page":"1493","DOI":"10.1016\/j.ic.2005.05.011","volume":"204","author":"M. Bozzano","year":"2006","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossumd, P., Sebastiani, R.: Efficient theory combination via Boolean search. Information and Computation\u00a0204(10), 1493\u20131525 (2006)","journal-title":"Information and Computation"},{"key":"14_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-642-00768-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Brummayer","year":"2009","unstructured":"Brummayer, R., Biere, A.: Boolector: An efficient SMT solver for bit-vectors and arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 174\u2013177. Springer, Heidelberg (2009)"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-540-70545-1_28","volume-title":"Computer Aided Verification","author":"R. Bruttomesso","year":"2008","unstructured":"Bruttomesso, R., Cimatti, A., Franz\u00e9n, A., Griggio, A., Sebastiani, R.: The mathSAT\u00a04 SMT solver. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol.\u00a05123, pp. 299\u2013303. Springer, Heidelberg (2008)"},{"issue":"1","key":"14_CR6","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/s10472-009-9152-7","volume":"55","author":"R. Bruttomesso","year":"2009","unstructured":"Bruttomesso, R., Cimatti, A., Franzen, A., Griggio, A., Sebastiani, R.: Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: A comparative analysis. Annals of Mathematics and Artificial Intelligence\u00a055(1), 63\u201399 (2009)","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"14_CR7","series-title":"Electronic Notes in Theoretical Computer Science","first-page":"37","volume-title":"5th International Workshop on Satisfiability Modulo Theories","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based Theory Combination. In: 5th International Workshop on Satisfiability Modulo Theories. Electronic Notes in Theoretical Computer Science, vol.\u00a0198, pp. 37\u201349. Elsevier, Amsterdam (2008)"},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"14_CR9","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1109\/FMCAD.2009.5351142","volume-title":"Formal Methods in Computer-Aided Design, 2009","author":"L. Moura de","year":"2009","unstructured":"de Moura, L., Bj\u00f8rner, N.: Generalized, efficient array decision procedures. In: Formal Methods in Computer-Aided Design, 2009, pp. 45\u201352. IEEE, Los Alamitos (2009)"},{"key":"14_CR10","unstructured":"Dutertre, B., de Moura, L.: The YICES SMT Solver (2006) Tool paper at, http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"14_CR11","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":"14_CR12","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. Technical Report TR2010-922, Department of Computer Science, New York University (January 2010)","DOI":"10.1007\/978-3-642-16242-8_29"},{"key":"14_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"402","DOI":"10.1007\/978-3-642-16242-8_29","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"D. Jovanovi\u0107","year":"2010","unstructured":"Jovanovi\u0107, D., Barrett, C.: Polite theories revisited. In: Ferm\u00fcller, C.G., Voronkov, A. (eds.) LPAR-17. LNCS, vol.\u00a06397, pp. 402\u2013416. Springer, Heidelberg (2010)"},{"key":"14_CR14","doi-asserted-by":"crossref","unstructured":"Jovanovi\u0107, D., Barrett, C.: Sharing is Caring: Combination of Theories. Technical Report TR2011-940, New York University (2011)","DOI":"10.1007\/978-3-642-24364-6_14"},{"issue":"2","key":"14_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 Transactions on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Transactions on Programming Languages and Systems"},{"issue":"3","key":"14_CR16","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"D.C. Oppen","year":"1980","unstructured":"Oppen, D.C.: Complexity, convexity and combinations of theories. Theoretical Computer Science\u00a012(3), 291\u2013302 (1980)","journal-title":"Theoretical Computer Science"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-93900-9_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"Z. Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107, Z., Hu, A.J.: A Scalable Memory Model for Low-Level Code. In: Jones, N.D., M\u00fcller-Olm, M. (eds.) VMCAI 2009. LNCS, vol.\u00a05403, pp. 290\u2013304. Springer, Heidelberg (2009)"},{"key":"14_CR18","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":"14_CR19","first-page":"526","volume-title":"5th International Joint Conference on Artificial Intelligence","author":"R.E. Shostak","year":"1977","unstructured":"Shostak, R.E.: An algorithm for reasoning about equality. In: 5th International Joint Conference on Artificial Intelligence, pp. 526\u2013527. Morgan Kaufmann Publishers Inc., San Francisco (1977)"},{"key":"14_CR20","series-title":"Applied Logic","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of Combining Systems","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.T.: A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Frontiers of Combining Systems. Applied Logic, pp. 103\u2013120. Kluwer Academic Publishers, Dordrecht (1996)"},{"key":"14_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logics in Artificial Intelligence","author":"C. Tinelli","year":"2004","unstructured":"Tinelli, C., Zarba, C.: Combining decision procedures for sorted theories. In: Alferes, J.J., Leite, J. (eds.) JELIA 2004. LNCS (LNAI), vol.\u00a03229, pp. 641\u2013653. Springer, Heidelberg (2004)"}],"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_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,16]],"date-time":"2019-06-16T14:00:14Z","timestamp":1560693614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-24364-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642243639","9783642243646"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-24364-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}