{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:09:37Z","timestamp":1725487777471},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540678632"},{"type":"electronic","value":"9783540446590"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44659-1_12","type":"book-chapter","created":{"date-parts":[[2007,7,21]],"date-time":"2007-07-21T17:40:26Z","timestamp":1185039626000},"page":"179-196","source":"Crossref","is-referenced-by-count":11,"title":["Reachability Programming in HOL98 Using BDDs"],"prefix":"10.1007","author":[{"given":"Michael J. C.","family":"Gordon","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"12_CR1","doi-asserted-by":"crossref","unstructured":"Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Combining theorem proving and trajectory evaluation in an industrial environment. In Design Automation Conference (DAC), pages 538\u2013541. ACM\/IEEE, July 1998.","DOI":"10.1145\/277044.277189"},{"key":"12_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics (TPHOLs99)","author":"M. D. Aagaard","year":"1999","unstructured":"Mark D. Aagaard, Robert B. Jones, and Carl-Johan H. Seger. Lifted-FL: A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Theorem Proving in Higher Order Logics (TPHOLs99), number 1690 in Lecture Notes in Computer Science, pages 323\u2013340. Springer-Verlag, 1999."},{"issue":"3","key":"12_CR3","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1145\/136035.136043","volume":"24","author":"R. E. Bryant","year":"1992","unstructured":"Randall E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computing Surveys, 24(3):293\u2013318, September 1992.","journal-title":"ACM Computing Surveys"},{"key":"12_CR4","unstructured":"E. Charniak, C. K. Riesbeck, and D. V. McDermott. Artificial Intelligence Programming. Lawrence Erlbaum Associates, 1980."},{"key":"12_CR5","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation","author":"M. J. C. Gordon","year":"1979","unstructured":"M. J. C. Gordon, R. Milner, and C. P. Wadsworth. Edinburgh LCF: A Mechanised Logic of Computation, volume 78 of Lecture Notes in Computer Science. Springer-Verlag, 1979."},{"key":"12_CR6","unstructured":"Mike Gordon. Programming combinations of deduction and BDD-based symbolic calculation. Technical Report 480, University of Cambridge Computer Laboratory, December 1999."},{"key":"12_CR7","unstructured":"Mike Gordon and Ken Friis Larsen. Combining the Hol98 proof assistant with the BuDDy BDD package. Technical Report 481, University of Cambridge Computer Laboratory, December 1999."},{"key":"12_CR8","doi-asserted-by":"crossref","unstructured":"Scott Hazelhurst and Carl-Johan H. Seger. Symbolic trajectory evaluation. In Thomas Kropf, editor, Formal Hardware Verification, chapter 1, pages 3\u201378. Springer-Verlag, 1997.","DOI":"10.1007\/3-540-63475-4_1"},{"key":"12_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1007\/3-540-57826-9_135","volume-title":"Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG\u201993, Vancouver, B.C., August 11\u201313 1993","author":"J. Joyce","year":"1994","unstructured":"J. Joyce and C. Seger. The HOL-Voss System: Model-Checking inside a General-Purpose Theorem-Prover. In J. J. Joyce and C.-J. H. Seger, editors, Higher Order Logic Theorem Proving and its Applications: 6th International Workshop, HUG\u201993, Vancouver, B.C., August 11\u201313 1993, volume 780 of Lecture Notes in Computer Science, pages 185\u2013198. Spinger-Verlag, 1994."},{"key":"12_CR10","unstructured":"Edmund M. Clarke Jr. and Orna Grumberg. Model Checking. The MIT Press, 1999."},{"key":"12_CR11","unstructured":"Trevor W. S. Lee, Mark R. Greenstreet, and Carl-Johan Seger. Automatic verification of asynchronous circuits. Technical Report UBC TR 93-40, The University of British Columbia, November 1993."},{"key":"12_CR12","unstructured":"K. L. McMillan. A methodology for hardware verification using compositional model checking. Technical report, Cadence Berkeley Labs, April 1999. Available at http:\/\/www-cad.eecs.berkeley.edu\/~kenmcmil\/ ."},{"key":"12_CR13","doi-asserted-by":"crossref","unstructured":"Kenneth L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"12_CR14","unstructured":"John O\u2019Leary, Xudong Zhao, Robert Gerth, and Carl-Johan H. Seger. Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal, First Quarter 1999. Online at http:\/\/developer.intel.com\/technology\/itj\/ ."},{"key":"12_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification, CAV\u2019 95","author":"S. Rajan","year":"1995","unstructured":"S. Rajan, N. Shankar, and M.K. Srivas. An integration of model-checking with automated proof checking. In Pierre Wolper, editor, Computer-Aided Verification, CAV\u2019 95, volume 939 of Lecture Notes in Computer Science, pages 84\u201397, Liege, Belgium, June 1995. Springer-Verlag."},{"key":"12_CR16","unstructured":"Carl-Johan H. Seger. Voss-a formal hardware verification system: User\u2019s guide. Technical Report UBC TR 93-45, The University of British Columbia, December 1993."}],"container-title":["Lecture Notes in Computer Science","Theorem Proving in Higher Order Logics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44659-1_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T11:32:54Z","timestamp":1556710374000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44659-1_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540678632","9783540446590"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-44659-1_12","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}