{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T19:22:29Z","timestamp":1648581749279},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2012,6,9]],"date-time":"2012-06-09T00:00:00Z","timestamp":1339200000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Methods Syst Des"],"published-print":{"date-parts":[[2013,2]]},"DOI":"10.1007\/s10703-012-0159-z","type":"journal-article","created":{"date-parts":[[2012,6,8]],"date-time":"2012-06-08T12:59:29Z","timestamp":1339160369000},"page":"67-90","source":"Crossref","is-referenced-by-count":3,"title":["Being careful about theory combination"],"prefix":"10.1007","volume":"42","author":[{"given":"Dejan","family":"Jovanovi\u0107","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2012,6,9]]},"reference":[{"key":"159_CR1","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"512","DOI":"10.1007\/11916277_35","volume-title":"Logic for programming, artificial intelligence, and reasoning","author":"C Barrett","year":"2006","unstructured":"Barrett C, Nieuwenhuis R, Oliveras A, Tinelli C (2006) Splitting on demand in SAT modulo theories. In: Logic for programming, artificial intelligence, and reasoning. LNCS, vol 4246. Springer, Berlin, pp\u00a0512\u2013526"},{"key":"159_CR2","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"298","DOI":"10.1007\/978-3-540-73368-3_34","volume-title":"CVC3. In computer aided verification","author":"C Barrett","year":"2007","unstructured":"Barrett C, Tinelli C (2007) CVC3. In computer aided verification. LNCS, vol 4590. Springer, Berlin, pp\u00a0298\u2013302"},{"issue":"10","key":"159_CR3","doi-asserted-by":"crossref","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 (2006) Efficient theory combination via Boolean search. Inf Comput 204(10):1493\u20131525","journal-title":"Inf Comput"},{"key":"159_CR4","series-title":"LNCS","doi-asserted-by":"crossref","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 (2009) Boolector: an efficient SMT solver for bit-vectors and arrays. In: Tools and algorithms for the construction and analysis of systems. LNCS, vol 5505. Springer, Berlin, pp 174\u2013177"},{"key":"159_CR5","series-title":"LNCS","doi-asserted-by":"crossref","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 (2008) The MathSAT 4 SMT solver. In: Computer aided verification. LNCS, vol 5123. Springer, Berlin, pp 299\u2013303"},{"issue":"1","key":"159_CR6","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1007\/s10472-009-9152-7","volume":"55","author":"R Bruttomesso","year":"2009","unstructured":"Bruttomesso R, Cimatti A, Franz\u00e9n A, Griggio A, Sebastiani R (2009) Delayed theory combination vs. Nelson-Oppen for satisfiability modulo theories: a comparative analysis. Ann Math Artif Intell 55(1):63\u201399","journal-title":"Ann Math Artif Intell"},{"key":"159_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 (2008) Model-based theory combination. In: 5th international workshop on satisfiability modulo theories. Electronic notes in theoretical computer science, vol 198. Elsevier, Amsterdam, pp\u00a037\u201349"},{"key":"159_CR8","series-title":"LNCS","doi-asserted-by":"crossref","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 (2008) Z3: an efficient SMT solver. In: Tools and algorithms for the construction and analysis of systems. LNCS, vol 4963. Springer, Berlin, p 337"},{"key":"159_CR9","first-page":"45","volume-title":"Formal methods in computer-aided design","author":"L Moura de","year":"2009","unstructured":"de Moura L, Bj\u00f8rner N (2009) Generalized, efficient array decision procedures. In: Formal methods in computer-aided design. IEEE, New York, pp 45\u201352"},{"key":"159_CR10","unstructured":"Dutertre B, de Moura L (2006) The YICES SMT solver. Tool paper at http:\/\/yices.csl.sri.com\/tool-paper.pdf"},{"key":"159_CR11","volume-title":"A mathematical introduction to logic","author":"HB Enderton","year":"1972","unstructured":"Enderton HB (1972) A mathematical introduction to logic. Academic Press, New York"},{"key":"159_CR12","unstructured":"Jovanovi\u0107 D, Barrett C (2010) Technical Report TR2010-922, Department of Computer Science, New York University, January 2010"},{"key":"159_CR13","series-title":"LNCS","doi-asserted-by":"crossref","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 (2010) Polite theories revisited. In: Logic for programming, artificial intelligence, and reasoning. LNCS, vol 6397. Springer, Berlin, pp 402\u2013416"},{"key":"159_CR14","doi-asserted-by":"crossref","first-page":"195","DOI":"10.1007\/978-3-642-24364-6_14","volume-title":"Frontiers of combining systems","author":"D Jovanovi\u0107","year":"2011","unstructured":"Jovanovi\u0107 D, Barrett C (2011) Sharing is caring: combination of theories. In: Frontiers of combining systems, pp 195\u2013210"},{"issue":"2","key":"159_CR15","doi-asserted-by":"crossref","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G Nelson","year":"1979","unstructured":"Nelson G, Oppen DC (1979) Simplification by cooperating decision procedures. ACM Trans Program Lang Syst 1(2):245\u2013257","journal-title":"ACM Trans Program Lang Syst"},{"issue":"3","key":"159_CR16","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1016\/0304-3975(80)90059-6","volume":"12","author":"DC Oppen","year":"1980","unstructured":"Oppen DC (1980) Complexity, convexity and combinations of theories. Theor Comput Sci 12(3):291\u2013302","journal-title":"Theor Comput Sci"},{"key":"159_CR17","series-title":"LNCS","first-page":"304","volume-title":"Verification, model checking, and abstract interpretation","author":"Z Rakamari\u0107","year":"2009","unstructured":"Rakamari\u0107 Z, Hu AJ (2009) A scalable memory model for low-level code. In: Verification, model checking, and abstract interpretation. LNCS, vol 5403. Springer, Berlin, p 304"},{"key":"159_CR18","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"48","DOI":"10.1007\/11559306_3","volume-title":"Frontiers of combining systems","author":"S Ranise","year":"2005","unstructured":"Ranise S, Ringeissen C, Calogero GZ (2005) Combining data structures with nonstably infinite theories using many-sorted logic. In: Frontiers of combining systems. LNCS, vol 3717. Springer, Berlin, pp 48\u201364"},{"key":"159_CR19","first-page":"526","volume-title":"5th international joint conference on artificial intelligence","author":"RE Shostak","year":"1977","unstructured":"Shostak RE (1977) An algorithm for reasoning about equality. In: 5th international joint conference on artificial intelligence. Morgan Kaufmann, San Mateo, pp 526\u2013527"},{"key":"159_CR20","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-94-009-0349-4_5","volume-title":"Frontiers of combining systems, applied logic","author":"C Tinelli","year":"1996","unstructured":"Tinelli C, Harandi MT (1996) A new correctness proof of the Nelson\u2013Oppen combination procedure. In: Frontiers of combining systems, applied logic. Kluwer Academic, Dordrecht, pp 103\u2013120"},{"key":"159_CR21","series-title":"LNAI","doi-asserted-by":"crossref","first-page":"641","DOI":"10.1007\/978-3-540-30227-8_53","volume-title":"Logic in artificial intelligence","author":"C Tinelli","year":"2004","unstructured":"Tinelli C, Zarba C (2004) Combining decision procedures for sorted theories. In: Logic in artificial intelligence. LNAI, vol 3229. Springer, Berlin, pp 641\u2013653"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0159-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-012-0159-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-012-0159-z","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,30]],"date-time":"2019-05-30T22:05:52Z","timestamp":1559253952000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-012-0159-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,6,9]]},"references-count":21,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2013,2]]}},"alternative-id":["159"],"URL":"https:\/\/doi.org\/10.1007\/s10703-012-0159-z","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2012,6,9]]}}}