{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,9,22]],"date-time":"2026-09-22T11:58:15Z","timestamp":1790078295545,"version":"4.0.1"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540787990","type":"print"},{"value":"9783540788003","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2008]]},"DOI":"10.1007\/978-3-540-78800-3_24","type":"book-chapter","created":{"date-parts":[[2008,4,2]],"date-time":"2008-04-02T04:26:19Z","timestamp":1207110379000},"page":"337-340","source":"Crossref","is-referenced-by-count":4586,"title":["Z3: An Efficient SMT Solver"],"prefix":"10.1007","author":[{"given":"Leonardo","family":"de Moura","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikolaj","family":"Bj\u00f8rner","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"issue":"1","key":"24_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/565816.503274","volume":"37","author":"T. Ball","year":"2002","unstructured":"Ball, T., Rajamani, S.K.: The SLAM project: debugging system software via static analysis. SIGPLAN Not.\u00a037(1), 1\u20133 (2002)","journal-title":"SIGPLAN Not."},{"key":"24_CR2","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":"24_CR3","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1095810.1095824","volume-title":"SOSP","author":"M. Costa","year":"2005","unstructured":"Costa, M., Crowcroft, J., Castro, M., Rowstron, A.I.T., Zhou, L., Zhang, L., Barham, P.: Vigilante: end-to-end containment of internet worms. In: Herbert, A., Birman, K.P. (eds.) SOSP, pp. 133\u2013147. ACM Press, New York (2005)"},{"key":"24_CR4","series-title":"Lecture Notes in Artificial Intelligence","first-page":"183","volume-title":"Automated Deduction \u2013 CADE-21","author":"N.S. Bj\u00f8rner","year":"2007","unstructured":"Bj\u00f8rner, N.S., de Moura, L.: Efficient E-Matching for SMT Solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"24_CR5","unstructured":"de Moura, L., Bj\u00f8rner, N.: Model-based Theory Combination. In: SMT 2007 (2007)"},{"key":"24_CR6","unstructured":"\u00a0de\u00a0Moura, L., and \u00a0Bj\u00f8rner, N.: Relevancy Propagation. Technical Report MSR-TR-2007-140, Microsoft Research (2007)"},{"key":"24_CR7","unstructured":"DeLine, R., Leino, K.R.M.: BoogiePL: A typed procedural language for checking object-oriented programs. Technical Report 2005-70, Microsoft Research (2005)"},{"issue":"3","key":"24_CR8","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":"24_CR9","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":"24_CR10","doi-asserted-by":"crossref","first-page":"117","DOI":"10.1145\/1181775.1181790","volume-title":"SIGSOFT FSE","author":"B.S. Gulavani","year":"2006","unstructured":"Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: Synergy: a new algorithm for property checking. In: Young, M., Devanbu, P.T. (eds.) SIGSOFT FSE, pp. 117\u2013127. ACM, New York (2006)"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"Lahiri, S.K., Qadeer, S.: Back to the Future: Revisiting Precise Program Verification using SMT Solvers. In: POPL 2008 (2008)","DOI":"10.1145\/1328438.1328461"},{"key":"24_CR12","unstructured":"Ranise, S., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2006), http:\/\/www.SMT-LIB.org"},{"key":"24_CR13","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1109\/MS.2006.117","volume":"23","author":"N. Tillmann","year":"2006","unstructured":"Tillmann, N., Schulte, W.: Unit Tests Reloaded: Parameterized Unit Testing with Symbolic Execution. IEEE software\u00a023, 38\u201347 (2006)","journal-title":"IEEE software"}],"container-title":["Lecture Notes in Computer Science","Tools and Algorithms for the Construction and Analysis of Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-78800-3_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,17]],"date-time":"2023-05-17T07:35:18Z","timestamp":1684308918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-78800-3_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008]]},"ISBN":["9783540787990","9783540788003"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2008]]}}}