{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T16:57:41Z","timestamp":1791046661474,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":12,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540439974","type":"print"},{"value":"9783540456575","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45657-0_40","type":"book-chapter","created":{"date-parts":[[2007,5,19]],"date-time":"2007-05-19T10:59:43Z","timestamp":1179572383000},"page":"500-504","source":"Crossref","is-referenced-by-count":85,"title":["CVC: A Cooperating Validity Checker"],"prefix":"10.1007","author":[{"given":"Aaron","family":"Stump","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Clark W.","family":"Barrett","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2002,9,20]]},"reference":[{"key":"40_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1007\/BFb0031808","volume-title":"Formal Methods In Computer-Aided Design","author":"C. Barrett","year":"1996","unstructured":"C. Barrett, D. Dill, and J. Levitt. Validity checking for combinations of theories with equality. In M. Srivas and A. Camilleri, editors, Formal Methods In Computer-Aided Design, volume 1166 of LNCS, pages 187\u2013201. Springer-Verlag, 1996."},{"key":"40_CR2","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. A Framework for Cooperating Decision Procedures. In David McAllester, editor, 17th International Conference on Computer Aided Deduction, volume 1831 of LNAI, pages 79\u201397. Springer-Verlag, 2000.","DOI":"10.1007\/10721959_6"},{"key":"40_CR3","doi-asserted-by":"crossref","unstructured":"C. Barrett, D. Dill, and A. Stump. Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT. In 14th International Conference on Computer-Aided Verification, 2002.","DOI":"10.1007\/3-540-45657-0_18"},{"key":"40_CR4","doi-asserted-by":"crossref","unstructured":"J. Filli\u00e2tre, S. Owre, H. Rue\u00df, and N. Shankar. ICS: integrated canonizer and solver. In G. Berry, H. Comon, and A. Finkel, editors, 13th International Conference on Computer-Aided Verification, 2001.","DOI":"10.1007\/3-540-44585-4"},{"issue":"1","key":"40_CR5","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R. Harper","year":"1993","unstructured":"R. Harper, F. Honsell, and G. Plotkin. A Framework for Defining Logics. Journal of the Association for Computing Machinery, 40(1):143\u2013184, January 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"40_CR6","doi-asserted-by":"crossref","unstructured":"M. Moskewicz, C. Madigan, Y. Zhaod, L. Zhang, and S. Malik. Chaff: Engineering an Efficient SAT Solver. In 39th Design Automation Conference, 2001.","DOI":"10.1145\/378239.379017"},{"issue":"2","key":"40_CR7","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1145\/357073.357079","volume":"1","author":"G. Nelson","year":"1979","unstructured":"G. Nelson and D. Oppen. Simplification by cooperating decision procedures. ACM Transactions on Programming Languages and Systems, 1(2):245\u201357, 1979.","journal-title":"ACM Transactions on Programming Languages and Systems"},{"key":"40_CR8","doi-asserted-by":"crossref","unstructured":"S. Owre, J. Rushby, and N. Shankar. PVS: A Prototype Verification System. In D. Kapur, editor, 11th International Conference on Automated Deduction, volume607 of LNAI, pages 748\u2013752. Springer-Verlag, 1992.","DOI":"10.1007\/3-540-55602-8_217"},{"key":"40_CR9","doi-asserted-by":"crossref","unstructured":"J. Skakkeb\u00e6k, R. Jones, and D. Dill. Formal verification of out-of-order execution using incremental flushing. In 10th International Conference on Computer Aided Verification, 1998.","DOI":"10.21236\/ADA400401"},{"key":"40_CR10","doi-asserted-by":"crossref","unstructured":"A. Stump, C. Barrett, D. Dill, and J. Levitt. A Decision Procedure for an Extensional Theory of Arrays. In 16th IEEE Symposium on Logic in Computer Science, pages 29\u201337. IEEE Computer Society, 2001.","DOI":"10.1109\/LICS.2001.932480"},{"key":"40_CR11","doi-asserted-by":"crossref","unstructured":"A. Stump and D. Dill. Faster Proof Checking in the Edinburgh Logical Framework. In 18th International Conference on Automated Deduction, 2002.","DOI":"10.1007\/3-540-45620-1_32"},{"key":"40_CR12","doi-asserted-by":"crossref","unstructured":"A. Stump and D. Dill. Producing Proofs from an Arithmetic Decision Procedure in Elliptical LF. In 3rd International Workhsop on Logical Frameworks and Meta-Languages, 2002. (acceptance pending).","DOI":"10.1016\/S1571-0661(04)80504-8"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45657-0_40","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T01:21:11Z","timestamp":1556414471000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45657-0_40"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439974","9783540456575"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/3-540-45657-0_40","relation":{},"ISSN":["0302-9743"],"issn-type":[{"value":"0302-9743","type":"print"}],"subject":[],"published":{"date-parts":[[2002]]}}}