{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T22:23:49Z","timestamp":1725488629313},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540664635"},{"type":"electronic","value":"9783540482567"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1999]]},"DOI":"10.1007\/3-540-48256-3_20","type":"book-chapter","created":{"date-parts":[[2007,8,3]],"date-time":"2007-08-03T20:15:22Z","timestamp":1186172122000},"page":"293-310","source":"Crossref","is-referenced-by-count":4,"title":["Importing MDG Verification Results into HOL"],"prefix":"10.1007","author":[{"given":"Haiyan","family":"Xiong","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sofi\u00e8ne","family":"Tahar","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[1999,9,17]]},"reference":[{"key":"20_CR1","doi-asserted-by":"crossref","unstructured":"R. E. Bryant. Symbolic boolean manipulation with ordered binary-decision diagrams. ACM Computer Surveys, 24(3), September 1992.","DOI":"10.1145\/136035.136043"},{"issue":"1","key":"20_CR2","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008663530211","volume":"10","author":"F. Corella","year":"1997","unstructured":"F. Corella, Z. Zhou, X. Song, M. Langevin, and E. Cerny. Multiway decision-graphs for automated hardware verification. Formal Methods in System Design, 10(1):7\u201346, 1997.","journal-title":"Formal Methods in System Design"},{"key":"20_CR3","doi-asserted-by":"crossref","unstructured":"P. Curzon. The formal verification of the Fairisle ATM switching element. Technical Report 329, University of Cambridge, Computer Laboratory, March 1994.","DOI":"10.1145\/197917.198171"},{"key":"20_CR4","doi-asserted-by":"crossref","unstructured":"P. Curzon. Tracking design changes with formal machine-checked proof. The Computer Journal, 38(2), July 1995.","DOI":"10.1093\/comjnl\/38.2.91"},{"key":"20_CR5","unstructured":"P. Curzon, S. Tahar, and O. A\u00eft-Mohamed. The verification of aspects of a decision diagram based verification system. In Jim Grundy and Malcolm Newey, editors, Theorem Proving in Higher-Order Logics: Emerging Trends, pages 31\u201346. Department of Computer Science, The Australian National University, 1998."},{"key":"20_CR6","unstructured":"M. J. C. Gordon. Why higher-order logic is a good formalism for specifying and verifying hardware. In G. J. Milne and P. A. Subrahmanyam, editors, Formal Aspects of VLSI Design: the 1985 Edinburgh Workshop on VLSI, pages 153\u2013177. North-Holland, 1986."},{"key":"20_CR7","unstructured":"M. J. C. Gordon. Combining deductive theorem proving with symbolic state enumeration. Presented at 21 Years of Hardware Verification, Royal Society Workshop to mark 21 years of BCS FACS, http:\/\/www.cl.cam.ac.uk\/users\/mjcg\/BDD , December 1998."},{"key":"20_CR8","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":"20_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"662","DOI":"10.1007\/3-540-60973-3_113","volume-title":"Formal methods Europe FME\u2019 96","author":"K. Havelund","year":"1996","unstructured":"K. Havelund and N. Shankar. Experiments in theorem proving and model checking for protocol verification. In Formal methods Europe FME\u2019 96, number 1051 in Lecture Notes in Computer Science, pages 662\u2013682, March 1996."},{"key":"20_CR10","doi-asserted-by":"crossref","unstructured":"J. Joyce and C. Seger. Linking BDD-based symbolic evaluation to interactive theorem-proving. In the 30th Design Automation Conference, 1993.","DOI":"10.1145\/157485.164981"},{"key":"20_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/3-540-60045-0_42","volume-title":"Computer-Aided Verification","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, number 939 in Lecture Notes in Computer Science, pages 84\u201397. Springer-Verlag, 1995."},{"key":"20_CR12","unstructured":"S. Tahar and P. Curzon. Comparing HOL and MDG: A case study on the verification of an ATM switch fabric. To appear in the Nordic Journal of Computing."},{"key":"20_CR13","unstructured":"S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin, and O. A\u00eft-Mohamed. Modeling and automatic formal verification of the Fairisle ATM switch fabric using MDGs. To appear in IEEE Transactions on CAD of Integrated Circuits and Systems."},{"key":"20_CR14","unstructured":"H. Xiong and P. Curzon. The verification of a translator for MDG\u2019s components in HOL. In MUCORT98, Third Middlesex University Conference on Research in Technology, pages 55\u201359, April 1998."},{"key":"20_CR15","unstructured":"Z. Zhou and N. Boulerice. MDG Tools (V1.0) User Manual. University of Montreal, Dept. D\u2019IRO, 1996."},{"key":"20_CR16","series-title":"Lect Notes Comput Sci","first-page":"252","volume-title":"Higher-Order Logic theorem proving and Its Applications, The 6th International Workshop","author":"Z. Zhu","year":"1993","unstructured":"Z. Zhu, J. Joyce, and C. Seger. Verification of the Tamarack-3 microprocessor in a hybrid verification environment. In Higher-Order Logic theorem proving and Its Applications, The 6th International Workshop, number 780 in Lecture Notes in Computer Science, pages 252\u2013266. B. C., Canada, August 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-48256-3_20","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,1]],"date-time":"2019-05-01T18:58:36Z","timestamp":1556737116000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-48256-3_20"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1999]]},"ISBN":["9783540664635","9783540482567"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-48256-3_20","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1999]]}}}