{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,24]],"date-time":"2026-01-24T23:40:11Z","timestamp":1769298011035,"version":"3.49.0"},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540733676","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-73368-3_34","type":"book-chapter","created":{"date-parts":[[2007,8,29]],"date-time":"2007-08-29T22:29:34Z","timestamp":1188426574000},"page":"298-302","source":"Crossref","is-referenced-by-count":188,"title":["CVC3"],"prefix":"10.1007","author":[{"given":"Clark","family":"Barrett","sequence":"first","affiliation":[]},{"given":"Cesare","family":"Tinelli","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"34_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"515","DOI":"10.1007\/978-3-540-27813-9_49","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, pp. 515\u2013518. Springer, Heidelberg (2004)"},{"key":"34_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1007\/11513988_29","volume-title":"Computer Aided Verification","author":"C. Barrett","year":"2005","unstructured":"Barrett, C., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 291\u2013295. Springer, Heidelberg (2005)"},{"key":"34_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","DOI":"10.1007\/11916277_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"C. Barrett","year":"2006","unstructured":"Barrett, C., Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Splitting on demand in SAT modulo theories. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol.\u00a04246, Springer, Heidelberg (2006)"},{"key":"34_CR4","doi-asserted-by":"crossref","unstructured":"Barrett, C., Shikanian, I., Tinelli, C.: An abstract decision procedure for satisfiability in the theory of recursive data types. In: PDPAR (2006)","DOI":"10.1016\/j.entcs.2006.11.037"},{"key":"34_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods in Computer-Aided Design","author":"C.W. Barrett","year":"1996","unstructured":"Barrett, C.W., Dill, D.L., Levitt, J.R.: Validity checking for combinations of theories with equality. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol.\u00a01166, pp. 187\u2013201. Springer, Heidelberg (1996)"},{"key":"34_CR6","unstructured":"Detlefs, D.L., Nelson, G., Saxe, J.B.: Simplify: A theorem-prover for program checking. Technical Report HPL-2003-148, HP System Research Center (2003)"},{"key":"34_CR7","series-title":"Lecture Notes in Computer Science","volume-title":"Theory and Applications of Satisfiability Testing","author":"N. E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible sat-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol.\u00a02919, Springer, Heidelberg (2004)"},{"key":"34_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"15","DOI":"10.1007\/978-3-540-30482-1_10","volume-title":"Formal Methods and Software Engineering","author":"J.-C. Filli\u00e2tre","year":"2004","unstructured":"Filli\u00e2tre, J.-C., March\u00e9, C.: Multi-Prover Verification of C Programs. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol.\u00a03308, pp. 15\u201329. Springer, Heidelberg (2004)"},{"key":"34_CR9","unstructured":"Ge, Y., Barrett, C., Tinelli, C.: Solving quantified verification condisions using satisfiability modulo theories. In: CADE 2007 (to appear, July 2007)"},{"key":"34_CR10","doi-asserted-by":"crossref","unstructured":"McLaughlin, S., Barrett, C., Ge, Y.: Cooperating theorem provers: A case study combining HOL-Light and CVC Lite. In: PDPAR, pp. 43\u201351 (2006)","DOI":"10.1016\/j.entcs.2005.12.005"},{"key":"34_CR11","doi-asserted-by":"crossref","unstructured":"Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: Engineering an Efficient SAT Solver. In: DAC (2001)","DOI":"10.1145\/378239.379017"},{"key":"34_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"500","DOI":"10.1007\/3-540-45657-0_40","volume-title":"Computer Aided Verification","author":"A. Stump","year":"2002","unstructured":"Stump, A., Barrett, C.W., Dill, D.L.: CVC: A cooperating validity checker. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 500\u2013504. Springer, Heidelberg (2002)"},{"key":"34_CR13","doi-asserted-by":"crossref","unstructured":"Tiu, A., Barsotti, D., Prensa, L.: Verification of clock synchronization algorithms: Experiments on a combination of deductive tools. In: AVOCS (2005)","DOI":"10.1016\/j.entcs.2005.10.005"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-73368-3_34.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T10:08:32Z","timestamp":1619518112000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-73368-3_34"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540733676"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-73368-3_34","relation":{},"subject":[]}}