{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T06:40:30Z","timestamp":1725518430073},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540710691"},{"type":"electronic","value":"9783540710707"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-71070-7_40","type":"book-chapter","created":{"date-parts":[[2008,8,29]],"date-time":"2008-08-29T05:56:30Z","timestamp":1219989390000},"page":"475-490","source":"Crossref","is-referenced-by-count":25,"title":["Engineering DPLL(T) + Saturation"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"40_CR1","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\u2013Putnam\u2013Logemann\u2013Loveland procedure to DPLL(T). J. ACM\u00a053, 937\u2013977 (2006)","journal-title":"J. ACM"},{"key":"40_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, 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"40_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73595-3_12","volume-title":"Automated Deduction \u2013 CADE-21","author":"Y. Ge","year":"2007","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification conditions using satisfiability modulo theories. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603. Springer, Heidelberg (2007)"},{"key":"40_CR4","unstructured":"Moskal, M., Lopuszanski, J., Kiniry, J.R.: E-matching for fun and profit. In: Satisfiability Modulo Theories Workshop (2007)"},{"key":"40_CR5","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":"40_CR6","doi-asserted-by":"crossref","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: TACAS 2008 (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"40_CR7","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Reasoning","author":"E. Denney","year":"2004","unstructured":"Denney, E., Fischer, B., Schumann, J.: Using automated theorem provers to certify auto-generated aerospace software. In: Basin, D., Rusinowitch, M. (eds.) IJCAR 2004. LNCS (LNAI), vol.\u00a03097. Springer, Heidelberg (2004)"},{"key":"40_CR8","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: ESCoR Workshop (2006)"},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"Deharbe, D., Ranise, S.: Satisfiability solving for software verification. International Journal on Software Tools Technology Transfer (to appear, 2008)","DOI":"10.1007\/s10009-009-0105-6"},{"key":"40_CR10","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1016\/B978-044450813-3\/50004-7","volume-title":"Handbook of Automated Reasoning","author":"L. Bachmair","year":"2001","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Handbook of Automated Reasoning, pp. 19\u201399. MIT Press, Cambridge (2001)"},{"key":"40_CR11","volume-title":"Handbook of Automated Reasoning","author":"R. Nieuwenhuis","year":"2001","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning. MIT Press, Cambridge (2001)"},{"key":"40_CR12","unstructured":"de Moura, L., Bj\u00f8rner, N.: Relevancy Propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)"},{"key":"40_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-61040-5","volume-title":"Rewriting Techniques and Applications","author":"P. Graf","year":"1995","unstructured":"Graf, P.: Substitution tree indexing. In: Hsiang, J. (ed.) RTA 1995. LNCS, vol.\u00a0914. Springer, Heidelberg (1995)"},{"key":"40_CR14","unstructured":"Schulz, S.: Simple and Efficient Clause Subsumption with Feature Vector Indexing. In: ESFOR Workshop (2004)"},{"key":"40_CR15","unstructured":"Baumgartner, P., Fuchs, A., Tinelli, C.: Darwin: A theorem prover for the model evolution calculus. In: ESFOR Workshop (2004)"},{"key":"40_CR16","doi-asserted-by":"crossref","unstructured":"Gallier, J., Narendran, P., Plaisted, D., Raatz, S., Snyder, W.: An algorithm for finding canonical sets of ground rewrite rules in polynomial time. J. ACM\u00a040 (1993)","DOI":"10.1145\/138027.138032"},{"key":"40_CR17","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 $\\sharp$ 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":"40_CR18","first-page":"111","volume":"15","author":"S. Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun\u00a015, 111\u2013126 (2002)","journal-title":"AI Commun"},{"key":"40_CR19","series-title":"Lecture Notes in Artificial Intelligence","volume-title":"Automated Deduction - CADE-18","author":"C. Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol.\u00a02392, Springer, Heidelberg (2002)"},{"key":"40_CR20","doi-asserted-by":"crossref","unstructured":"Lynch, C.: SMELS: Satisfiability Modulo Equality with Lazy Superposition. The Dagsthul Seminar on Deduction and Decision Procedures (2007)","DOI":"10.1007\/978-3-540-88387-6_15"},{"key":"40_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-540-74915-8_19","volume-title":"Computer Science Logic","author":"K. Korovin","year":"2007","unstructured":"Korovin, K., Voronkov, A.: Integrating linear arithmetic into superposition calculus. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol.\u00a04646, pp. 223\u2013237. Springer, Heidelberg (2007)"},{"key":"40_CR22","unstructured":"Fietzke, A.: Labelled splitting. Master\u2019s thesis, Saarland University (2007)"},{"key":"40_CR23","unstructured":"Riazanov, A., Voronkov, A.: Splitting without backtracking. In: IJCAI (2001)"},{"key":"40_CR24","doi-asserted-by":"crossref","unstructured":"Armando, A., Bonacina, M.P., Ranise, S., Schulz, S.: New results on rewrite-based satisfiability procedures. ACM Transactions on Computational Logic (to appear)","DOI":"10.1145\/1459010.1459014"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-71070-7_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T13:42:03Z","timestamp":1557754923000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-71070-7_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540710691","9783540710707"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-71070-7_40","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2008]]}}}