{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:14:47Z","timestamp":1725455687715},"publisher-location":"Berlin\/Heidelberg","reference-count":11,"publisher":"Springer-Verlag","isbn-type":[{"type":"print","value":"3540544771"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0023718","type":"book-chapter","created":{"date-parts":[[2005,11,19]],"date-time":"2005-11-19T01:01:03Z","timestamp":1132362063000},"page":"44-53","source":"Crossref","is-referenced-by-count":2,"title":["Vectorized model checking for computation tree logic"],"prefix":"10.1007","author":[{"given":"Hiromi","family":"Hiraishi","sequence":"first","affiliation":[]},{"given":"Shintaro","family":"Meki","sequence":"additional","affiliation":[]},{"given":"Kiyoharu","family":"Hamaguchi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","unstructured":"A. V. Aho, J. E. Hopcroft, and J. D. Ullman. The Design and Analysis of Computer Algorithms. Addison Wesley, 1974."},{"key":"6_CR2","unstructured":"M. C. Browne. An improved algorithm for the automatic verification of finite state systems using temporal logic. Technical Report CMU-CS-86-156, Carnegie Mellon University, 1986."},{"issue":"12","key":"6_CR3","doi-asserted-by":"crossref","first-page":"1035","DOI":"10.1109\/TC.1986.1676711","volume":"C-35","author":"M. C. Browne","year":"1986","unstructured":"M. C. Browne, E. M. Clarke, D. L. Dill, and B. Mishra. Automatic verification of sequential circuits using temporal logic. IEEE Transactions on Computers, C-35(12):1035\u20131044, December 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"6_CR4","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, 1990."},{"key":"6_CR5","unstructured":"E. M. Clarke, S. Bose, M. C. Browne, and O. Grumberg. The design and verification of finite state hardware controllers. Technical Report CMU-CS-87-145, Carnegie Mellon University, July 1987."},{"key":"6_CR6","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":"6_CR7","doi-asserted-by":"crossref","unstructured":"E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite state concurrent systems using temporal logic specifications: A practical approach. Technical Report CMU-CS-83-152, Carnegie Mellon University, 1983.","DOI":"10.1145\/567067.567080"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"E. M. Clarke and O. Grumberg. Avoiding the state explosion problem in temporal logic model checking algorithms. In Proc. 6th Annual ACM Symposium of Principles of Distributed Computing, pages 294\u2013303, August 1987.","DOI":"10.1145\/41840.41865"},{"key":"6_CR9","unstructured":"E. M. Clarke and O. Grumberg. Research on automatic verification of finite-state concurrent systems. Technical Report CMU-CS-87-105, Carnegie Mellon University, January 1987."},{"key":"6_CR10","unstructured":"E. M. Clarke, D. E. Long, and K. L. McMillan. A language for compositional specification and verification of finite state hardware controllers. In Proc. 9th IFIP Symposium on Computer Hardware Description Languages and their Applications, pages 281\u2013295, June 1989."},{"key":"6_CR11","doi-asserted-by":"crossref","unstructured":"S. Graf, J. L. Richier, C. Rodriguez, and J. Voiron. What are the limits of model checking methods for the verification of real life protocols? In Proc. Workshop on Automatic Verification Methods for Finite State Systems, June 1989.","DOI":"10.1007\/3-540-52148-8_23"}],"container-title":["Lecture Notes in Computer Science","Computer-Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0023718.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T16:50:14Z","timestamp":1607532614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0023718"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540544771"],"references-count":11,"URL":"https:\/\/doi.org\/10.1007\/bfb0023718","relation":{},"subject":[]}}