{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T00:42:54Z","timestamp":1761957774650,"version":"build-2065373602"},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2009,2,1]],"date-time":"2009-02-01T00:00:00Z","timestamp":1233446400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Ann Math Artif Intell"],"published-print":{"date-parts":[[2009,2]]},"DOI":"10.1007\/s10472-009-9153-6","type":"journal-article","created":{"date-parts":[[2009,7,15]],"date-time":"2009-07-15T07:57:05Z","timestamp":1247644625000},"page":"101-122","source":"Crossref","is-referenced-by-count":18,"title":["Solving quantified verification conditions using satisfiability modulo theories"],"prefix":"10.1007","volume":"55","author":[{"given":"Yeting","family":"Ge","sequence":"first","affiliation":[]},{"given":"Clark","family":"Barrett","sequence":"additional","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2009,7,16]]},"reference":[{"key":"9153_CR1","doi-asserted-by":"crossref","first-page":"445","DOI":"10.1016\/B978-044450813-3\/50010-2","volume-title":"Handbook of Automated Reasoning, vol. I, chapter 8","author":"F Baader","year":"2001","unstructured":"Baader, F., Snyder, W.: Unification theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol.\u00a0I, chapter\u00a08, pp. 445\u2013532. Elsevier Science, Amsterdam (2001)"},{"key":"9153_CR2","doi-asserted-by":"crossref","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. Technical report 06-05, Department of Computer Science, The University of Iowa (2006)","DOI":"10.1007\/11916277_35"},{"key":"9153_CR3","unstructured":"Barrett, C., Ranise, S., Stump, A., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org (2008)"},{"key":"9153_CR4","first-page":"298","volume-title":"Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907), Berlin, Germany. Lecture Notes in Computer Science, vol. 4590","author":"C Barrett","year":"2007","unstructured":"Barrett, C., Tinelli, C.: CVC3. In: Damm, W., Hermanns, H. (eds.) Proceedings of the 19th International Conference on Computer Aided Verification (CAV\u201907), Berlin, Germany. Lecture Notes in Computer Science, vol. 4590, pp. 298\u2013302. Springer, New York (2007)"},{"key":"9153_CR5","unstructured":"Barrett, C.W.: Checking validity of quantifier-free formulas in combinations of first-order theories. Ph.D. thesis, Stanford University (2003)"},{"key":"9153_CR6","first-page":"132","volume-title":"Proc. FroCoS \u201902. LNAI, vol. 2309","author":"CW Barrett","year":"2002","unstructured":"Barrett, C.W., Dill, D.L., Stump, A.: A generalization of Shostak\u2019s method for combining decision procedures. In: Armando, A. (ed.) Proc. FroCoS \u201902. LNAI, vol. 2309, pp. 132\u2013146. Springer, New York (2002)"},{"key":"9153_CR7","doi-asserted-by":"crossref","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. Artif. Intell. 172, 591\u2013632 (2008)","journal-title":"Artif. Intell."},{"key":"9153_CR8","first-page":"183","volume-title":"CADE. Lecture Notes in Computer Science, vol. 4603","author":"LM Moura de","year":"2007","unstructured":"de\u00a0Moura, L.M., Bj\u00f8rner, N.: Efficient E-matching for SMT solvers. In: Pfenning, F. (ed.) CADE. Lecture Notes in Computer Science, vol. 4603, pp. 183\u2013198. Springer, New York (2007)"},{"key":"9153_CR9","first-page":"198","volume-title":"IJCAR. LNCS, vol. 3097","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.A., Rusinowitch, M. (eds.) IJCAR. LNCS, vol. 3097, pp. 198\u2013212. Springer, New York (2004)"},{"issue":"3","key":"9153_CR10","doi-asserted-by":"crossref","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 52(3), 365\u2013473 (2005)","journal-title":"J. ACM"},{"key":"9153_CR11","unstructured":"Flanagan, C., Joshi, R., Saxe, J.B.: An explicating theorem prover for quantified formulas. Technical report HPL-2004-199, HP Intelligent Enterprise Technologies Laboratory (2004)"},{"key":"9153_CR12","doi-asserted-by":"crossref","unstructured":"Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B.: Extended static checking for Java. In: Proc. ACM Conference on Programming Language Design and Implementation, pp. 234\u2013245 (2002)","DOI":"10.1145\/512529.512558"},{"key":"9153_CR13","first-page":"175","volume-title":"Proceedings of the 16th International Conference on Computer Aided Verification, CAV\u201904 (Boston, Massachusetts). LNCS, vol. 3114","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. (eds.) Proceedings of the 16th International Conference on Computer Aided Verification, CAV\u201904 (Boston, Massachusetts). LNCS, vol. 3114, pp. 175\u2013188. Springer, New York (2004)"},{"issue":"4","key":"9153_CR14","doi-asserted-by":"crossref","first-page":"371","DOI":"10.1023\/A:1015854101244","volume":"28","author":"J Hooker","year":"2002","unstructured":"Hooker, J., Rago, G., Chandru, V., Shrivastava, A.: Partial instantiation methods for inference in first order logic. J. Autom. Reason. 28(4), 371\u2013396 (2002)","journal-title":"J. Autom. Reason."},{"key":"9153_CR15","unstructured":"Moskal, M., Lopuszanski, J., Kiniry, J.: E-matching for fun and profit. In: Krstic, S., Oliveras, A. (eds.) Proceedings of the 5th International Workshop on Satisfiability Modulo Theories (SMT \u201907), pp. 25\u201335. Berlin, Germany (2007)"},{"issue":"6","key":"9153_CR16","doi-asserted-by":"crossref","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-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53(6), 937\u2013977 (2006)","journal-title":"J. ACM"},{"issue":"3","key":"9153_CR17","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1023\/A:1006376231563","volume":"25","author":"DA Plaisted","year":"2000","unstructured":"Plaisted, D.A., Zhu, Y.: Ordered semantic hyper linking. J. Autom. Reason. 25(3), 167\u2013217 (2000)","journal-title":"J. Autom. Reason."},{"key":"9153_CR18","unstructured":"Prevosto, V., Waldmann, U.: SPASS+T. In: Sutcliffe, G., Schmidt, R., Schulz, S. (eds.) Proceedings of ESCoR: Empirically Successful Computerized Reasoning, Seattle, WA. CEUR Workshop Proceedings, vol. 192, pp. 18\u201333 (2006)"},{"issue":"2\u20133","key":"9153_CR19","first-page":"91","volume":"15","author":"A Riazanov","year":"2002","unstructured":"Riazanov, A., Voronkov, A.: The design and implementation of VAMPIRE. AI Commun. 15(2\u20133), 91\u2013110 (2002)","journal-title":"AI Commun."},{"issue":"4","key":"9153_CR20","doi-asserted-by":"crossref","first-page":"333","DOI":"10.1007\/BF00244275","volume":"1","author":"ME Stickel","year":"1985","unstructured":"Stickel, M.E.: Automated deduction by theory resolution. J. Autom. Reason. 1(4), 333\u2013355 (1985)","journal-title":"J. Autom. Reason."},{"issue":"1","key":"9153_CR21","first-page":"33","volume":"18","author":"G Sutcliffe","year":"2005","unstructured":"Sutcliffe, G.: The IJCAR-2004 automated theorem proving competition. AI Commun. 18(1), 33\u201340 (2005)","journal-title":"AI Commun."},{"issue":"2","key":"9153_CR22","doi-asserted-by":"crossref","first-page":"177","DOI":"10.1023\/A:1005806324129","volume":"21","author":"G Sutcliffe","year":"1998","unstructured":"Sutcliffe, G., Suttner, C.: The TPTP problem library: CNF release v1.2.1. J. Autom. Reason. 21(2), 177\u2013203 (1998)","journal-title":"J. Autom. Reason."},{"key":"9153_CR23","first-page":"275","volume-title":"CADE. LNCS, vol. 2392","author":"C Weidenbach","year":"2002","unstructured":"Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobald, C., Topic, D.: SPASS version 2.0. In: Voronkov, A. (ed.) CADE. LNCS, vol. 2392, pp.\u00a0275\u2013279. Springer, New York (2002)"}],"container-title":["Annals of Mathematics and Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9153-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10472-009-9153-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10472-009-9153-6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,29]],"date-time":"2019-05-29T17:58:13Z","timestamp":1559152693000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10472-009-9153-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,2]]},"references-count":23,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2009,2]]}},"alternative-id":["9153"],"URL":"https:\/\/doi.org\/10.1007\/s10472-009-9153-6","relation":{},"ISSN":["1012-2443","1573-7470"],"issn-type":[{"type":"print","value":"1012-2443"},{"type":"electronic","value":"1573-7470"}],"subject":[],"published":{"date-parts":[[2009,2]]}}}