{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:01:49Z","timestamp":1725483709436},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540425410"},{"type":"electronic","value":"9783540447986"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2001]]},"DOI":"10.1007\/3-540-44798-9_21","type":"book-chapter","created":{"date-parts":[[2007,5,3]],"date-time":"2007-05-03T17:16:15Z","timestamp":1178212575000},"page":"244-258","source":"Crossref","is-referenced-by-count":4,"title":["Hierarchical Verification Using an MDG-HOL Hybrid Tool"],"prefix":"10.1007","author":[{"given":"Iskander","family":"Kort","sequence":"first","affiliation":[]},{"given":"Sofiene","family":"Tahar","sequence":"additional","affiliation":[]},{"given":"Paul","family":"Curzon","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2001,8,24]]},"reference":[{"key":"21_CR1","series-title":"Lect Notes Comput Sci","first-page":"400","volume-title":"Higher Order Logic Theorem Proving and Its Applications","author":"M.D. Aagaard","year":"1993","unstructured":"M.D. Aagaard, M. Leeser, and P. Windley. Toward a super duper hardware tactic. In J.J. Joyce and C.H. Seger, editors, Higher Order Logic Theorem Proving and Its Applications, LNCS 780, pages 400\u2013413. Springer-Verlag, 1993."},{"key":"21_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"323","DOI":"10.1007\/3-540-48256-3_22","volume-title":"Theorem Proving in Higher Order Logics","author":"M.D. Aagaard","year":"1999","unstructured":"M.D. Aagaard, R.B. Jones, and C-J.H. Seger. Lifted-FL:A Pragmatic Implementation of Combined Model Checking and Theorem Proving. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 323\u2013340. Springer-Verlag, 1999."},{"key":"21_CR3","doi-asserted-by":"crossref","unstructured":"S. Balakrishnan and S. Tahar. A Hierarchical Approach to the Formal Verification of Embedded Systems Using MDGs. In Proceedings IEEE 9th Great Lakes Symposium on VLSI, Ann Arbor, Michigan, USA, March 1999, pages 284\u2013287.","DOI":"10.1109\/GLSV.1999.757434"},{"issue":"1","key":"21_CR4","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":"21_CR5","unstructured":"P. Curzon, S. Tahar, and O. Ait-Mohamed. Verification of the MDG Components Library in HOL. In J. Grundy and M. Newey, editors, Theorem Proving in Higher Order Logics:Emerging Trends, pages 31\u201345, Australian National University, 1998."},{"key":"21_CR6","volume-title":"Technical Report","author":"P. Curzon","year":"1994","unstructured":"P. Curzon. The Formal Verification of the Fairisle ATM Switching Element. Technical Report 329, Computer Laboratory, University of Cambridge, U.K., 1994."},{"key":"21_CR7","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-46419-0_7","volume-title":"Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"L. A. Dennis","year":"2000","unstructured":"L. A. Dennis, G. Collins, M. Norrish, R. Boulton, K. Slind, G. Robinson, M. Gordon, and T. Melham. The PROSPER Toolkit. In Proceedings of the Sixth International Conference on Tools and Algorithms for the Construction and Analysis of Systems. LNCS 1785, Springer Verlag, 2000."},{"key":"21_CR8","unstructured":"M.J.C. Gordon. Combining Deductive Theorem Proving with Symbolic State Enumeration. 21 Years of Hardware Verification, December 1998. Royal Society Workshop to mark 21 years of BCS FACS."},{"key":"21_CR9","volume-title":"Introduction to HOL:A Theorem Proving Environment for Higher-Order Logic","author":"M.J.C. Gordon","year":"1993","unstructured":"M.J.C. Gordon and T.F. Melham. Introduction to HOL:A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, U.K., 1993."},{"key":"21_CR10","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1007\/3-540-48256-3_21","volume-title":"Theorem Proving in Higher Order Logics","author":"J. Hurd","year":"1999","unstructured":"J. Hurd. Integrating Gandalf and HOL. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, pages 311\u2013321. Springer Verlag, 1999."},{"key":"21_CR11","doi-asserted-by":"crossref","unstructured":"J.J. Joyce and C.J.H. Seger. Linking BDD-based Symbolic Evaluation to Interactive Theorem Proving. In Proceedings of the 30th Design Automation Conference, pages 469\u2013474, Dallas, TX, June 1993.","DOI":"10.1145\/157485.164981"},{"key":"21_CR12","doi-asserted-by":"publisher","first-page":"165","DOI":"10.1007\/BF01383880","volume":"2","author":"R. Kumar","year":"1993","unstructured":"R. Kumar, K. Schneider and T. Kropf. Structuring and Automating Hardware Proofs in a Higher-Order Theorem-Proving Environment. Formal Methods in System Design, 2:165\u2013223, 1993.","journal-title":"Formal Methods in System Design"},{"issue":"4","key":"21_CR13","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. A CM Communication Review, 19(4):327\u2013336, 1991.","journal-title":"A CM Communication Review"},{"key":"21_CR14","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","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, Lecture Notes in Computer Science 939, pages 84\u201397. Springer Verlag, 1995."},{"key":"21_CR15","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48256-3_17","volume-title":"Theorem Proving in Higher Order Logics","author":"K. Schneider","year":"1999","unstructured":"K. Schneider and D.W. Hoffmann. A HOL Conversion for Translating Linear Time Temporal Logic to \u00fa-Automata. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690. Springer Verlag, 1999."},{"issue":"7","key":"21_CR16","doi-asserted-by":"publisher","first-page":"956","DOI":"10.1109\/43.771178","volume":"18","author":"S. Tahar","year":"1999","unstructured":"S. Tahar, X. Song, E. Cerny, Z. Zhou, M. Langevin and O. Ait-Mohamed. Modeling and Verification of the Fairisle ATM Switch Fabric using MDGs. IEEE Transactions on CAD of Integrated Circuits and Systems, 18(7):956\u2013972, 1999.","journal-title":"IEEE Transactions on CAD of Integrated Circuits and Systems"},{"key":"21_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"293","DOI":"10.1007\/3-540-48256-3_20","volume-title":"Theorem Proving in Higher Order Logics","author":"H. Xiong","year":"1999","unstructured":"H. Xiong, P. Curzon, and S. Tahar. Importing MDG Results into HOL. In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery, editors, Theorem Proving in Higher Order Logics, LNCS 1690, 293\u2013310. Springer Verlag, 1999."},{"key":"21_CR18","unstructured":"M.H. Zobair and S. Tahar. On the Modeling and Verification of a Telecom System Block Using MDGs. Technical Report, Concordia University, Department of Electrical and Computer Engineering, December 2000."}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44798-9_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,2,16]],"date-time":"2019-02-16T12:39:12Z","timestamp":1550320752000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44798-9_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001]]},"ISBN":["9783540425410","9783540447986"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-44798-9_21","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2001]]}}}