{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,13]],"date-time":"2026-02-13T23:36:36Z","timestamp":1771025796401,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642385735","type":"print"},{"value":"9783642385742","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38574-2_26","type":"book-chapter","created":{"date-parts":[[2013,6,4]],"date-time":"2013-06-04T07:55:13Z","timestamp":1370332513000},"page":"377-391","source":"Crossref","is-referenced-by-count":39,"title":["Quantifier Instantiation Techniques for Finite Model Finding in SMT"],"prefix":"10.1007","author":[{"given":"Andrew","family":"Reynolds","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]},{"given":"Amit","family":"Goel","sequence":"additional","affiliation":[]},{"given":"Sava","family":"Krsti\u0107","sequence":"additional","affiliation":[]},{"given":"Morgan","family":"Deters","sequence":"additional","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press (1998)","DOI":"10.1017\/CBO9781139172752"},{"key":"26_CR2","doi-asserted-by":"publisher","first-page":"591","DOI":"10.1016\/j.artint.2007.09.005","volume":"172","author":"P. Baumgartner","year":"2008","unstructured":"Baumgartner, P., Tinelli, C.: The Model Evolution calculus as a first-order DPLL method. Artificial Intelligence\u00a0172, 591\u2013632 (2008)","journal-title":"Artificial Intelligence"},{"key":"26_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"183","DOI":"10.1007\/978-3-540-73595-3_13","volume-title":"Automated Deduction \u2013 CADE-21","author":"L. Moura de","year":"2007","unstructured":"de Moura, L., Bj\u00f8rner, N.S.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol.\u00a04603, pp. 183\u2013198. Springer, Heidelberg (2007)"},{"key":"26_CR4","unstructured":"Blanchette, J.C.: Personal communication (2013)"},{"key":"26_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-22438-6_11","volume-title":"Automated Deduction \u2013 CADE-23","author":"J.C. Blanchette","year":"2011","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending Sledgehammer with SMT solvers. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS, vol.\u00a06803, pp. 116\u2013130. Springer, Heidelberg (2011)"},{"key":"26_CR6","unstructured":"Claessen, K., S\u00f6rensson, N.: New techniques that improve MACE-style finite model building. In: CADE-19 Workshop: Model Computation \u2013 Principles, Algorithms, Applications, pp. 11\u201327 (2003)"},{"key":"26_CR7","unstructured":"Ganzinger, H., Korovin, K.: New directions in instantiation-based theorem proving. In: Proceedings of LICS 2003, pp. 55\u201364. IEEE Computer Society (2003)"},{"key":"26_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"306","DOI":"10.1007\/978-3-642-02658-4_25","volume-title":"Computer Aided Verification","author":"Y. Ge","year":"2009","unstructured":"Ge, Y., de Moura, L.: Complete instantiation for quantified formulas in satisfiabiliby modulo theories. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 306\u2013320. Springer, Heidelberg (2009)"},{"key":"26_CR9","unstructured":"Goel, A., Krstic, S., Tuttle, R.L.M.: SMT-based system verification with DVF. In: Proceedings of SMT 2012 (2012)"},{"key":"26_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"368","DOI":"10.1007\/978-3-642-02658-4_29","volume-title":"Computer Aided Verification","author":"S. Jacobs","year":"2009","unstructured":"Jacobs, S.: Incremental instance generation in local reasoning. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 368\u2013382. Springer, Heidelberg (2009)"},{"key":"26_CR11","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"292","DOI":"10.1007\/978-3-540-71070-7_24","volume-title":"Automated Reasoning","author":"K. Korovin","year":"2008","unstructured":"Korovin, K.: iProver \u2013 an instantiation-based theorem prover for first-order logic (System description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol.\u00a05195, pp. 292\u2013298. Springer, Heidelberg (2008)"},{"key":"26_CR12","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-74621-8_1","volume-title":"Frontiers of Combining Systems","author":"S. Krsti\u0107","year":"2007","unstructured":"Krsti\u0107, S., Goel, A.: Architecting solvers for SAT modulo theories: Nelson-Oppen with DPLL. In: Konev, B., Wolter, F. (eds.) FroCos 2007. LNCS (LNAI), vol.\u00a04720, pp. 1\u201327. Springer, Heidelberg (2007)"},{"key":"26_CR13","unstructured":"Reynolds, A., Tinelli, C., Goel, A., Krsti\u0107, S.: Finite model finding in SMT. In: Proceedings of CAV 2013. LNCS. Springer (accepted, 2013)"},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"Tuttle, M.R., Goel, A.: Protocol proof checking simplified with SMT. In: Proceedings of NCA 2012, pp. 195\u2013202. IEEE Computer Society (2012)","DOI":"10.1109\/NCA.2012.46"},{"key":"26_CR15","unstructured":"Zhang, J., Zhang, H.: SEM: a system for enumerating models. In: Proceedings of IJCAI 1995, pp. 298\u2013303 (1995)"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE-24"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38574-2_26","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T17:47:57Z","timestamp":1557769677000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38574-2_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642385735","9783642385742"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38574-2_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}