{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T23:00:56Z","timestamp":1725663656137},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540551799"},{"type":"electronic","value":"9783540467632"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1992]]},"DOI":"10.1007\/3-540-55179-4_21","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T09:51:10Z","timestamp":1330249870000},"page":"214-224","source":"Crossref","is-referenced-by-count":4,"title":["Vectorized symbolic model checking of computation tree logic for sequential machine verification"],"prefix":"10.1007","author":[{"given":"Hiromi","family":"Hiraishi","sequence":"first","affiliation":[]},{"given":"Kiyoharu","family":"Hamaguchi","sequence":"additional","affiliation":[]},{"given":"Hiroyuki","family":"Ochi","sequence":"additional","affiliation":[]},{"given":"Shuzo","family":"Yajima","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,29]]},"reference":[{"issue":"6","key":"21_CR1","doi-asserted-by":"crossref","first-page":"509","DOI":"10.1109\/TC.1978.1675141","volume":"C-27","author":"S. B. Akers","year":"1978","unstructured":"S. B. Akers. Binary decision diagrams. IEEE Transactions on Computers, C-27(6):509\u2013516, June 1978.","journal-title":"IEEE Transactions on Computers"},{"key":"21_CR2","doi-asserted-by":"crossref","unstructured":"K. S. Brace, R. L. Rudell, and R. E. Bryant. Efficient implementation of a BDD package. In Proc. 27th Design Automation Conference, pages 40\u201345, June 1990.","DOI":"10.1145\/123186.123222"},{"issue":"8","key":"21_CR3","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":"21_CR4","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Representing circuits more efficiently in symbolic model checking. In Proc. 28th Design Automation Conference, June 1991.","DOI":"10.1145\/127601.127702"},{"key":"21_CR5","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. Technical report, Carnegie Mellon University, November 1989.","DOI":"10.1145\/123186.123223"},{"key":"21_CR6","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 Proc. 27th Design Automation Conference, pages 46\u201351, June 1990.","DOI":"10.1145\/123186.123223"},{"key":"21_CR7","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and J. Hwang. Symbolic model checking: 1020 states and beyond. In Proc. Logic in Computer Science, June 1990."},{"key":"21_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and E. A. Emerson. Synthesis of synchronization skeletons for branching time temporal logic. In Proc. Workshop on Logic of Programs, pages 52\u201371. Springer-Verlag, 1981.","DOI":"10.1007\/BFb0025774"},{"key":"21_CR9","unstructured":"O. Coudert, C. Berthet, and J. C. Madre. Verification of sequential machines using functional vectors. In Proc. IMEC-IFIP Intrn. Workshop on Applied Formal Methods for Correct VLSI Design, pages 111\u2013128, November 1989."},{"key":"21_CR10","unstructured":"O. Coudert, J. C. Madre, and C. Berthet. Verifying temporal properties of sequential machines without building their state diagrams. In Proc. Workshop on Computer-Aided Verification, June 1990."},{"key":"21_CR11","unstructured":"N. Ishiura and S. Yajima. A class of logic functions expressible by polynomialsize binary decision diagrams. In Proc. the Synthesis and Simulation Meeting and International Interchange, pages 48\u201354, October 1990."},{"key":"21_CR12","doi-asserted-by":"crossref","unstructured":"S. Kimura and E. M. Clarke. A parallel algorithm for constructing binary decision diagrams. In Proc. IEEE ICCD'90, September 1990.","DOI":"10.1109\/ICCD.1990.130209"},{"key":"21_CR13","doi-asserted-by":"crossref","unstructured":"S. Minato, N. Ishiura, and S. Yajima. Shared binary decision diagram with attributed edges for efficient boolean function manipulation. In Proc. 27th Design Automation Conference, pages 52\u201357, June 1990.","DOI":"10.1145\/123186.123225"},{"key":"21_CR14","doi-asserted-by":"crossref","unstructured":"H. Ochi, N. Ishiura, and S. Yajima. Breadth-first manipulation of SBDD of boolean functions for vector processing. In Proc. 28th Design Automation Conference, June 1991.","DOI":"10.1145\/127601.127704"},{"key":"21_CR15","doi-asserted-by":"crossref","unstructured":"H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A. Sangiovanni-Vincentelli. Implicit state enumeration of finite state machines using BDD's. In Proc. ICCAD, 1990.","DOI":"10.1109\/ICCAD.1990.129860"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-55179-4_21.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,28]],"date-time":"2021-04-28T01:28:15Z","timestamp":1619573295000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-55179-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1992]]},"ISBN":["9783540551799","9783540467632"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-55179-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1992]]}}}