{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T22:59:48Z","timestamp":1725663588092},"publisher-location":"Berlin, Heidelberg","reference-count":13,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540564966"},{"type":"electronic","value":"9783540475729"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1993]]},"DOI":"10.1007\/3-540-56496-9_17","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T11:12:10Z","timestamp":1330254730000},"page":"206-219","source":"Crossref","is-referenced-by-count":1,"title":["Design verification of a microprocessor using branching time regular temporal logic"],"prefix":"10.1007","author":[{"given":"Kiyoharu","family":"Hamaguchi","sequence":"first","affiliation":[]},{"given":"Hiromi","family":"Hiraishi","sequence":"additional","affiliation":[]},{"given":"Shuzo","family":"Yajima","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,30]]},"reference":[{"issue":"8","key":"17_CR1","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. 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":"17_CR2","doi-asserted-by":"crossref","unstructured":"Shinichi Minato, Nagisa Ishiura, and Shuzo Yajima. Shared Binary Decision Diagram with Attributed Edges for Efficient Boolean Function Manipulation. In Proceedings of 27th Design Automation Conference, pages 52\u201357, 1990.","DOI":"10.1145\/123186.123225"},{"key":"17_CR3","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient Implementation of a BDD Package. In Proceedings of 27th Design Automation Conference, pages 40\u201345, 1990.","DOI":"10.1145\/123186.123222"},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential Circuit Verification Using Symbolic Model Checking. In Proceedings of 27th Design Automation Conference, pages 46\u201351, 1990.","DOI":"10.1145\/123186.123223"},{"key":"17_CR5","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing Circuits More Efficiently in Symbolic Model Checking. In Proceedings of 28th Design Automation Conference, pages 403\u2013407, June 1991.","DOI":"10.1145\/127601.127702"},{"key":"17_CR6","doi-asserted-by":"crossref","unstructured":"H. Hiraishi, K. Hamaguchi, H. Ochi, and S. Yajima. Vectorized Symbolic Model Checking of Computation Tree Logic. In Workshop on Computer-Aided Verification, pages 279\u2013290, July 1991.","DOI":"10.1007\/BFb0023718"},{"key":"17_CR7","unstructured":"E. M. Clarke and O. Gr\u00fcmberg and D. E. Long. Model Checking and Abstraction. Technical report, Carnegie Mellon University, 1991. manuscript."},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"K. Hamaguchi, H. Hiraishi, and S. Yajima. Branching Time Regular Temporal Logic for Model Checking with Linear Time Complexity. In Workshop on Computer-Aided Verification, June 1990.","DOI":"10.1090\/dimacs\/003\/34"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, O. Gr\u00fcmberg, and R. P. Kurshan. A synthesis of two approaches for verifying finite state concurrent systems. In Logic at Botik '89, Symposium on Logical Foundations of Computer Science, volume 363 of Lecture Notes in Computer Science. Springer Verlag, July 1989.","DOI":"10.1007\/3-540-51237-3_7"},{"key":"17_CR10","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic Model Checking: 1020 States and Beyond. In Proceedings of 5th IEEE Symposium on Logic in Computer Science, June 1990."},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"H. Kanbara. KUE-CHIP:A Microprocessor for education of Computer Architecture and LSI design. In Proc. of IEEE ASIC Seminar & Exhibit, 1990.","DOI":"10.1109\/ASIC.1990.186160"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"J. R. Burch. Using BDDs to verify multipliers. In Proceedings of 28th Design Automation Conference, pages 408\u2013412, jun 1991.","DOI":"10.1145\/127601.127703"},{"key":"17_CR13","unstructured":"A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison-Wesley, 1974."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-56496-9_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:03:59Z","timestamp":1605647039000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-56496-9_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993]]},"ISBN":["9783540564966","9783540475729"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/3-540-56496-9_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1993]]}}}