{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T09:56:23Z","timestamp":1776333383634,"version":"3.51.2"},"publisher-location":"Berlin, Heidelberg","reference-count":27,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540735946","type":"print"},{"value":"9783540735953","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-73595-3_13","type":"book-chapter","created":{"date-parts":[[2007,8,30]],"date-time":"2007-08-30T09:31:33Z","timestamp":1188466293000},"page":"183-198","source":"Crossref","is-referenced-by-count":167,"title":["Efficient E-Matching for SMT Solvers"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","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)"},{"issue":"3","key":"13_CR2","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. J. ACM\u00a052(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"13_CR3","series-title":"Lecture Notes in Computer Science","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, Springer, Heidelberg (2004)"},{"key":"13_CR4","unstructured":"Moskal, M., Lopusza\u0144ski, J.: Fast quantifier reasoning with lazy proof explication (2006), http:\/\/nemerle.org\/~malekith\/smt\/smt-tr-1.pdf"},{"key":"13_CR5","unstructured":"Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical Report HPL-2004-199, HP Laboratories, Palo Alto (2004)"},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B. Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A Fast Linear-Arithmetic Solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 81\u201394. Springer, Heidelberg (2006)"},{"key":"13_CR7","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/11591191_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"T. Ball","year":"2005","unstructured":"Ball, T., Lahiri, S.K., Musuvathi, M.: Zap: Automated theorem proving for software analysis. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 2\u201322. Springer, Heidelberg (2005)"},{"key":"13_CR8","unstructured":"Nelson, G.: Techniques for program verification. Technical Report CSL81-10, Xerox Palo Alto Research Center (1981)"},{"key":"13_CR9","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for java. In: PLDI, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"13_CR10","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report 2005-70, Microsoft Research (2005)"},{"key":"13_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"49","DOI":"10.1007\/978-3-540-30569-9_3","volume-title":"Construction and Analysis of Safe, Secure, and Interoperable Smart Devices","author":"M. Barnett","year":"2005","unstructured":"Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol.\u00a03362, pp. 49\u201369. Springer, Heidelberg (2005)"},{"key":"13_CR12","doi-asserted-by":"crossref","unstructured":"Kozen, D.: Complexity of finitely presented algebras. In: STOC, pp. 164\u2013177 (1977)","DOI":"10.1145\/800105.803406"},{"issue":"1","key":"13_CR13","doi-asserted-by":"publisher","first-page":"120","DOI":"10.1145\/321679.321689","volume":"19","author":"J.R. Slagle","year":"1972","unstructured":"Slagle, J.R.: Automatic theorem proving with built-in theories including equality, partial ordering, and sets. J. of the ACM\u00a019(1), 120\u2013135 (1972)","journal-title":"J. of the ACM"},{"issue":"4","key":"13_CR14","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"M.E. Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. J. Autom. Reasoning\u00a01(4), 333\u2013355 (1985)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/3-540-48958-4_4","volume-title":"Logic-Based Program Synthesis and Transformation","author":"J.V. Baalen","year":"1999","unstructured":"Baalen, J.V., Roach, S.: Using decision procedures to accelerate domain-specific deductive synthesis systems. In: Flener, P. (ed.) LOPSTR 1998. LNCS, vol.\u00a01559, pp. 61\u201382. Springer, Heidelberg (1999)"},{"key":"13_CR16","unstructured":"Waldmann, U., Prevosto, V.: SPASS+T. In: ESCoR, pp. 18\u201333 (2006)"},{"key":"13_CR17","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11559306_4","volume-title":"Frontiers of Combining Systems","author":"A. Armando","year":"2005","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: On a rewriting approach to satisfiability procedures: Extension, combination of theories and an experimental appraisal. In: Gramlich, B. (ed.) Frontiers of Combining Systems. LNCS (LNAI), vol.\u00a03717, pp. 65\u201380. Springer, Heidelberg (2005)"},{"key":"13_CR18","unstructured":"de Moura, L., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. Technical report, Microsoft Research (to appear)"},{"key":"13_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/7160.001.0001","volume-title":"Warren\u2019s abstract machine: a tutorial reconstruction","author":"H. A\u00eft-Kaci","year":"1991","unstructured":"A\u00eft-Kaci, H.: Warren\u2019s abstract machine: a tutorial reconstruction. MIT Press, Cambridge (1991)"},{"issue":"2","key":"13_CR20","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/BF00881918","volume":"15","author":"A. Voronkov","year":"1995","unstructured":"Voronkov, A.: The anatomy of vampire implementing bottom-up procedures with code trees. J. Autom. Reasoning\u00a015(2), 237\u2013265 (1995)","journal-title":"J. Autom. Reasoning"},{"key":"13_CR21","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"376","DOI":"10.1007\/3-540-45744-5_29","volume-title":"Automated Reasoning","author":"A. Riazanov","year":"2001","unstructured":"Riazanov, A., Voronkov, A.: Vampire 1.1 (system description). In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 376\u2013380. Springer, Heidelberg (2001)"},{"key":"13_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"553","DOI":"10.1007\/3-540-61511-3_113","volume-title":"Automated Deduction - Cade-13","author":"P. Graf","year":"1996","unstructured":"Graf, P., Meyer, C.: Advanced indexing operations on substitution trees. In: McRobbie, M.A., Slaney, J.K. (eds.) Automated Deduction - Cade-13. LNCS, vol.\u00a01104, pp. 553\u2013567. Springer, Heidelberg (1996)"},{"key":"13_CR23","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"242","DOI":"10.1007\/3-540-45744-5_18","volume-title":"Automated Reasoning","author":"H. Ganzinger","year":"2001","unstructured":"Ganzinger, H., Nieuwenhuis, R., Nivela, P.: Context trees. In: Gor\u00e9, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol.\u00a02083, pp. 242\u2013256. Springer, Heidelberg (2001)"},{"issue":"7","key":"13_CR24","doi-asserted-by":"publisher","first-page":"422","DOI":"10.1145\/362686.362692","volume":"13","author":"B.H. Bloom","year":"1970","unstructured":"Bloom, B.H.: Space\/time trade-offs in hash coding with allowable errors. Commun. ACM\u00a013(7), 422\u2013426 (1970)","journal-title":"Commun. ACM"},{"key":"13_CR25","doi-asserted-by":"crossref","first-page":"466","DOI":"10.1007\/978-3-642-81955-1_28","volume-title":"Automation of Reasoning 2: Classical Papers on Computational Logic","author":"G.S. Tseitin","year":"1983","unstructured":"Tseitin, G.S.: On the complexity of derivation in propositional calculus. In: Automation of Reasoning 2: Classical Papers on Computational Logic, pp. 466\u2013483. Springer, Heidelberg (1983)"},{"key":"13_CR26","series-title":"Lecture Notes in Computer Science","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K.R.M. Leino","year":"2005","unstructured":"Leino, K.R.M., Musuvathi, M., Ou, X.: A two-tier technique for supporting quantifiers in a lazily proof-explicating theorem prover. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, Springer, Heidelberg (2005)"},{"key":"13_CR27","unstructured":"Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), http:\/\/www.SMT-LIB.org"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-21"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73595-3_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,26]],"date-time":"2020-04-26T06:15:51Z","timestamp":1587881751000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73595-3_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540735946","9783540735953"],"references-count":27,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73595-3_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}