{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T14:12:45Z","timestamp":1725631965457},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540615873"},{"type":"electronic","value":"9783540706410"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1996]]},"DOI":"10.1007\/bfb0105419","type":"book-chapter","created":{"date-parts":[[2011,11,9]],"date-time":"2011-11-09T16:17:00Z","timestamp":1320855420000},"page":"415-430","source":"Crossref","is-referenced-by-count":1,"title":["A comparison of MDG and HOL for hardware verification"],"prefix":"10.1007","author":[{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,4,29]]},"reference":[{"issue":"8","key":"27_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"R. Bryant. Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, August 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"27_CR2","doi-asserted-by":"crossref","unstructured":"B. Chen, M. Yamazaki and M. Fujita. Bug Identification of a Real Chip Design by Symbolic Model Checking. In Proc. of the Int. Conf. on Circuits And Systems, pages 132\u2013136, June 1994.","DOI":"10.1109\/EDTC.1994.326886"},{"key":"27_CR3","unstructured":"F. Corella, Z. Zhou, X. Song, M. Langevin and E. Cerny. Multiway Decision Graphs for Automated Hardware Verification. Formal Methods in System Design, To appear. Available as IBM research report RC19676(87224), July 1994."},{"issue":"2","key":"27_CR4","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1093\/comjnl\/38.2.91","volume":"38","author":"P. Curzon","year":"1995","unstructured":"P. Curzon. Tracking Design Changes with Formal Machine-checked Proof. The Computer Journal, 38(2):91\u2013100, July 1995.","journal-title":"The Computer Journal"},{"key":"27_CR5","doi-asserted-by":"crossref","unstructured":"P. Curzon and I.M. Leslie. A Case Study on Design for Provability. In Proc. of the Int. Conf. on Engineering of Complex Comput\u00e9r Systems, pages 59\u201362, IEEE Computer Society Press, November 1995.","DOI":"10.1109\/ICECCS.1995.479304"},{"key":"27_CR6","doi-asserted-by":"crossref","unstructured":"M.J.C. Gordon. HOL: A Proof Generating System for Higher-order Logic. In G. Birtwistle and P.A. Subrahmanyam, editors, VLSI Specification, Verification and Synthesis, pages 73\u2013128. Kluwer Academic Publishers, 1988.","DOI":"10.1007\/978-1-4613-2007-4_3"},{"key":"27_CR7","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL: A Theorem Proving Environment for Higher-order Logic. Cambridge University Press, 1993."},{"key":"27_CR8","unstructured":"J.M.J. Herbert. Case Study of the Cambridge Fast Ring ECL Chip using HOL. Technical Report 123, University of Cambridge, Computer Laboratory, February 1988."},{"key":"27_CR9","doi-asserted-by":"crossref","unstructured":"M. Langevin, S. Tahar, Z. Zhou, X. Song and E. Cerny. Behavioral Verification of an ATM Switch Fabric using Implicit Abstract State Enumeration. In Proc. of the Int. Conf. on Computer Design, IEEE Computer Society Press, October 1996.","DOI":"10.1109\/ICCD.1996.563526"},{"issue":"4","key":"27_CR10","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1145\/115994.116022","volume":"19","author":"I.M. Leslie","year":"1991","unstructured":"I.M. Leslie and D.R. McAuley. Fairisle: An ATM Network for the Local Area. ACM Communication Review, 19(4):327\u2013336, September 1991.","journal-title":"ACM Communication Review"},{"key":"27_CR11","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"27_CR12","unstructured":"K. Schneider and T. Kropf. Verifying Hardware Correctness by Combining Theorem Proving and Model Checking. In J. Alves-Foss, editor, International Workshop on Higher Order Logic Theorem Proving and Its Applications: B-Track: Short Presentations, pages 89\u2013104, August 1995."},{"key":"27_CR13","doi-asserted-by":"crossref","unstructured":"S. Tahar, Z. Zhou, X. Song, E. Cerny and M. Langevin. Formal Verification of an ATM Switch Fabric using Multiway Decision Graphs. In Proc. of the Great Lakes Symp. on VLSI, pages 106\u2013111, IEEE Computer Society Press, March 1996.","DOI":"10.1109\/GLSV.1996.497603"}],"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\/BFb0105419","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T08:04:44Z","timestamp":1550304284000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0105419"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1996]]},"ISBN":["9783540615873","9783540706410"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/bfb0105419","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1996]]}}}