{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:23:41Z","timestamp":1725549821190},"publisher-location":"Berlin, Heidelberg","reference-count":29,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540272311"},{"type":"electronic","value":"9783540316862"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11513988_34","type":"book-chapter","created":{"date-parts":[[2010,3,12]],"date-time":"2010-03-12T13:33:28Z","timestamp":1268400808000},"page":"335-349","source":"Crossref","is-referenced-by-count":28,"title":["Efficient Satisfiability Modulo Theories via Delayed Theory Combination"],"prefix":"10.1007","author":[{"given":"Marco","family":"Bozzano","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Bruttomesso","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alessandro","family":"Cimatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tommi","family":"Junttila","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvio","family":"Ranise","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"van Rossum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Roberto","family":"Sebastiani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"34_CR1","volume-title":"Solvable Cases of the Decision Problem","author":"W. Ackermann","year":"1954","unstructured":"Ackermann, W.: Solvable Cases of the Decision Problem. North Holland Pub. Co., Amsterdam (1954)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/11527695_2","volume-title":"Theory and Applications of Satisfiability Testing","author":"A. Armando","year":"2005","unstructured":"Armando, A., Castellini, C., Giunchiglia, E., Maratea, M.: A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints. In: Hoos, H.H., Mitchell, D.G. (eds.) SAT 2004. LNCS, vol.\u00a03542, pp. 16\u201329. Springer, Heidelberg (2005)"},{"key":"34_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"457","DOI":"10.1007\/978-3-540-27813-9_36","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2004","unstructured":"Ball, T., Cook, B., Lahiri, S.K., Zhang, L.: Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 457\u2013461. Springer, Heidelberg (2004)"},{"key":"34_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2004","unstructured":"Barrett, C., Berezin, S.: CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., Ranise, S., van Rossum, P., Sebastiani, R.: Efficient Theory Combination via Boolean Search. Technical Report T05-04-02, ITC-IRST (2005)","key":"34_CR5"},{"key":"34_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-540-31980-1_21","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M. Bozzano","year":"2005","unstructured":"Bozzano, M., Bruttomesso, R., Cimatti, A., Junttila, T., van Rossum, P., Schulz, S., Sebastiani, R.: An incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 317\u2013333. Springer, Heidelberg (2005)"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-540-30206-3_19","volume-title":"Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems","author":"S. Cotton","year":"2004","unstructured":"Cotton, S., Asarin, E., Maler, O., Niebert, P.: Some Progress in Satisfiability Checking for Difference Logic. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol.\u00a03253, pp. 263\u2013276. Springer, Heidelberg (2004)"},{"unstructured":"CVC, CVCL and SVC, \n                    \n                      http:\/\/verify.stanford.edu\/CVC,CVCL,SVC\n                    \n                    \n                  .","key":"34_CR8"},{"key":"34_CR9","volume-title":"Proc. SEFM\u201903","author":"D. Deharbe","year":"2003","unstructured":"Deharbe, D., Ranise, S.: Light-Weight Theorem Proving for Debugging and Verifying Units of Code. In: Proc. SEFM 2003. IEEE Computer Society Press, Los Alamitos (2003)"},{"unstructured":"Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: A Theorem Prover for Program Checking. Technical Report HPL-2003-148, HP Laboratories (2003)","key":"34_CR10"},{"key":"34_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/3-540-44585-4_22","volume-title":"Computer Aided Verification","author":"J.-C. Filli\u00e2tre","year":"2001","unstructured":"Filli\u00e2tre, J.-C., Owre, S., Rue\u00df, H., Shankar, N.: ICS: Integrated Canonizer and Solver. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 246. Springer, Heidelberg (2001)"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1007\/978-3-540-45069-6_34","volume-title":"Computer Aided Verification","author":"C. Flanagan","year":"2003","unstructured":"Flanagan, C., Joshi, R., Ou, X., Saxe, J.B.: Theorem Proving using Lazy Proof Explication. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 355\u2013367. Springer, Heidelberg (2003)"},{"key":"34_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/978-3-540-27813-9_14","volume-title":"Computer Aided Verification","author":"H. Ganzinger","year":"2004","unstructured":"Ganzinger, H., Hagen, G., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: DPLL(T): Fast decision procedures. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 175\u2013188. Springer, Heidelberg (2004)"},{"unstructured":"ICS, \n                    \n                      http:\/\/www.icansolve.com","key":"34_CR14"},{"key":"34_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/978-3-540-27813-9_24","volume-title":"Computer Aided Verification","author":"D. Kroening","year":"2004","unstructured":"Kroening, D., Ouaknine, J., Seshia, S.A., Strichman, O.: Abstraction-Based Satisfiability Solving of Presburger Arithmetic. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 308\u2013320. Springer, Heidelberg (2004)"},{"unstructured":"MATHSAT, \n                    \n                      http:\/\/mathsat.itc.it","key":"34_CR16"},{"key":"34_CR17","first-page":"530","volume-title":"Proc. DAC 2001","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: Proc. DAC 2001, pp. 530\u2013535. ACM, New York (2001)"},{"issue":"2","key":"34_CR18","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 Trans. on Programming Languages and Systems\u00a01(2), 245\u2013257 (1979)","journal-title":"ACM Trans. on Programming Languages and Systems"},{"key":"34_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-44881-0","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"R. Nieuwenhuis","year":"2003","unstructured":"Nieuwenhuis, R., Oliveras, A.: Congruence Closure with Integer Offsets. In: Y. Vardi, M., Voronkov, A. (eds.) LPAR 2003. LNCS, vol.\u00a02850, Springer, Heidelberg (2003)"},{"key":"34_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"372","DOI":"10.1007\/978-3-540-31862-0_27","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"S. Ranise","year":"2005","unstructured":"Ranise, S., Ringeissen, C., Tran, D.-K.: Nelson-Oppen, Shostak, and the Extended Canonizer: A Family Picture with a Newborn. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 372\u2013386. Springer, Heidelberg (2005)"},{"key":"34_CR21","first-page":"19","volume-title":"Proc. LICS 2001","author":"H. Rue\u00df","year":"2001","unstructured":"Rue\u00df, H., Shankar, N.: Deconstructing Shostak. In: Proc. LICS 2001, pp. 19\u201328. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"34_CR22","volume-title":"Proc. LICS 2004","author":"S.A. Seshia","year":"2004","unstructured":"Seshia, S.A., Bryant, R.E.: Deciding Quantifier-Free Presburger Formulas Using Parameterized Solution Bounds. In: Proc. LICS 2004. IEEE, Los Alamitos (2004)"},{"key":"34_CR23","volume-title":"DAC 2003","author":"S.A. Seshia","year":"2003","unstructured":"Seshia, S.A., Lahiri, S.K., Bryant, R.E.: A Hybrid SAT-Based Decision Procedure for Separation Logic with Uninterpreted Functions. In: DAC 2003. ACM, New York (2003)"},{"key":"34_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/3-540-45610-4_1","volume-title":"Rewriting Techniques and Applications","author":"N. Shankar","year":"2002","unstructured":"Shankar, N., Rue\u00df, H.: Combining Shostak Theories. In: Tison, S. (ed.) RTA 2002. LNCS, vol.\u00a02378, p. 1. Springer, Heidelberg (2002)"},{"key":"34_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36126-X_10","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Strichman","year":"2002","unstructured":"Strichman, O.: On Solving Presburger and Linear Arithmetic with SAT. In: Aagaard, M.D., O\u2019Leary, J.W. (eds.) FMCAD 2002. LNCS, vol.\u00a02517. Springer, Heidelberg (2002)"},{"key":"34_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/3-540-45657-0_16","volume-title":"Computer Aided Verification","author":"O. Strichman","year":"2002","unstructured":"Strichman, O., Seshia, S., Bryant, R.: Deciding separation formulas with SAT. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, p. 209. Springer, Heidelberg (2002)"},{"key":"34_CR27","volume-title":"Proc. FroCos 1996","author":"C. Tinelli","year":"1996","unstructured":"Tinelli, C., Harandi, M.: A New Correctness Proof of the Nelson-Oppen Combination Procedure. In: Proc. FroCos 1996. Kluwer Academic Publishers, Dordrecht (1996)"},{"unstructured":"TSAT++, \n                    \n                      http:\/\/www.ai.dist.unige.it\/Tsat","key":"34_CR28"},{"unstructured":"UCLID, \n                    \n                      http:\/\/www-2.cs.cmu.edu\/~uclid","key":"34_CR29"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11513988_34","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,3,12]],"date-time":"2019-03-12T20:47:04Z","timestamp":1552423624000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11513988_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540272311","9783540316862"],"references-count":29,"URL":"https:\/\/doi.org\/10.1007\/11513988_34","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}