{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:15:06Z","timestamp":1794348906538,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540746201","type":"print"},{"value":"9783540746218","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-74621-8_1","type":"book-chapter","created":{"date-parts":[[2007,8,22]],"date-time":"2007-08-22T07:46:32Z","timestamp":1187768792000},"page":"1-27","source":"Crossref","is-referenced-by-count":26,"title":["Architecting Solvers for SAT Modulo Theories: Nelson-Oppen with DPLL"],"prefix":"10.1007","author":[{"given":"Sava","family":"Krsti\u0107","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Amit","family":"Goel","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","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":"1_CR2","unstructured":"Barrett, C.: Checking Validity of Quantifier-free Formulas in Combinations of First-Order Theories. PhD thesis, Stanford University (2002)"},{"key":"1_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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.: Splitting on demand in SAT Modulo Theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, Springer, Heidelberg (2006)"},{"key":"1_CR4","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11814771_42","volume-title":"Automated Reasoning","author":"M.P. Bonacina","year":"2006","unstructured":"Bonacina, M.P., Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decidability and undecidability results for Nelson-Oppen and rewrite-based decision procedures. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, Springer, Heidelberg (2006)"},{"key":"1_CR5","doi-asserted-by":"crossref","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Ranise, S., Sebastiani, R.: Efficient theory combination via boolean search. Information and Computation\u00a0204(10), 1493\u20131525","DOI":"10.1016\/j.ic.2005.05.011"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_7","volume-title":"Computer Aided Verification","author":"R. Bryant","year":"2002","unstructured":"Bryant, R., Lahiri, S., Seshia, S.: Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, Springer, Heidelberg (2002)"},{"issue":"2","key":"1_CR7","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/j.tcs.2005.11.025","volume":"354","author":"S. Conchon","year":"2006","unstructured":"Conchon, S., Krsti\u0107, S.: Strategies for combining decision procedures. Theoretical Computer Science\u00a0354(2), 187\u2013210 (2006)","journal-title":"Theoretical Computer Science"},{"issue":"7","key":"1_CR8","doi-asserted-by":"publisher","first-page":"394","DOI":"10.1145\/368273.368557","volume":"5","author":"M. Davis","year":"1962","unstructured":"Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM\u00a05(7), 394\u2013397 (1962)","journal-title":"Commun. ACM"},{"issue":"3","key":"1_CR9","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1145\/1066100.1066102","volume":"52","author":"D. Detlefs","year":"2005","unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A theorem prover for program checking. Journal of the ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"Journal of the ACM"},{"key":"1_CR10","unstructured":"Dutertre, B., de Moura, L.: The Yices SMT solver. Technical report, SRI International (2006)"},{"key":"1_CR11","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensen, N.: An extensible SAT solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems (TACAS)","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A., Grundy, J., Tinelli, C.: Combined satisfiability modulo parametric theories. In: TSDM 2000. LNCS, vol.\u00a04424, Springer, Heidelberg (2007)"},{"key":"1_CR13","volume-title":"Foundations of Programming Languages","author":"J.C. Mitchell","year":"1996","unstructured":"Mitchell, J.C.: Foundations of Programming Languages. MIT Press, Cambridge (1996)"},{"key":"1_CR14","volume-title":"Conference on Design Automation (DAC)","author":"M.W. Moskewicz","year":"2001","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient sat solver. In: Conference on Design Automation (DAC), ACM Press, New York (2001)"},{"issue":"2","key":"1_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":"6","key":"1_CR16","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1145\/1217856.1217859","volume":"53","author":"R. Nieuwenhuis","year":"2006","unstructured":"Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT Modulo Theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). Journal of the ACM\u00a053(6), 937\u2013977 (2006)","journal-title":"Journal of the ACM"},{"key":"1_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","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.) Frontiers of Combining Systems. LNCS (LNAI), vol.\u00a03717, Springer, Heidelberg (2005)"},{"key":"1_CR18","unstructured":"Reynolds, J.C.: Types, abstraction and parametric polymorphism. In: Mason, R.E.A., (ed.) Information Processing: 9th World Computer Congress, pp. 513\u2013523. North-Holland (1983)"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Tinelli, C., Harandi, M.: A new correctness proof of the Nelson-Oppen combination procedure. In: Frontiers of Combining Systems (FroCoS), vol.\u00a03 of Applied Logic, pp. 103\u2013120 (1996)","DOI":"10.1007\/978-94-009-0349-4_5"},{"issue":"3","key":"1_CR20","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/s10817-005-5204-9","volume":"34","author":"C. Tinelli","year":"2005","unstructured":"Tinelli, C., Zarba, C.: Combining nonstably infinite theories. Journal of Automated Reasoning\u00a034(3), 209\u2013238 (2005)","journal-title":"Journal of Automated Reasoning"}],"container-title":["Lecture Notes in Computer Science","Frontiers of Combining Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-74621-8_1.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T06:30:39Z","timestamp":1619505039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-74621-8_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540746201","9783540746218"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8_1","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-74621-8","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}