{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:35:30Z","timestamp":1761597330001},"publisher-location":"Berlin, Heidelberg","reference-count":15,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540581796"},{"type":"electronic","value":"9783540484691"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-58179-0_53","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T15:25:12Z","timestamp":1330269912000},"page":"182-193","source":"Crossref","is-referenced-by-count":28,"title":["Methodology and system for practical formal verification of reactive hardware"],"prefix":"10.1007","author":[{"given":"Ilan","family":"Beer","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Daniel","family":"Geist","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Raanan","family":"Gewirtzman","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Yoeli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"15_CR1","unstructured":"I. Beer, \u201cFormal Verification of Hardware\u201d, M.Sc. Thesis, EE Department, Technion, 1992 (in Hebrew)."},{"key":"15_CR2","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, \u201cGraph-Based Algorithms for Boolean Function Manipulation\u201d, IEEE Trans. Computers, Vol. C-35, August 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"15_CR3","unstructured":"E.M. Clarke and E.A. Emerson, \u201cDesign and Synthesis of Synchronization Skeletons using Branching Time Temporal Logic\u201d, in: Proceedings of the Workshop on Logic of Programs, LNCS 131, 1981. Temporal Logic Specifications: A Practical Approach\u201d, Tenth ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983."},{"key":"15_CR4","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson and A.P. Sistla, \u201cAutomatic Verification of Finite-State Concurrent Systems using Temporal Logic Specifications: A Practical Approach\u201d, Tenth ACM Symposium on Principles of Programming Languages, Austin, Texas, 1983.","DOI":"10.1145\/567067.567080"},{"issue":"1","key":"15_CR5","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/BF00571463","volume":"2","author":"M. Clint","year":"1973","unstructured":"M. Clint, \u201cProgram Proving: Coroutines\u201d, Acta informatica, 2(1), 50\u201363, 1973.","journal-title":"Acta informatica"},{"key":"15_CR6","unstructured":"E.A. Emerson, \u201cTemporal and Modal Logic\u201d, in: Handbook of Theoretical Computer Science, J. van Leeuwen, ed., North-Holland, 1989."},{"key":"15_CR7","doi-asserted-by":"crossref","unstructured":"D. Geist and I. Beer, \u201cEfficient Model Checking by Automated Ordering of Transition Relation Partitions\u201d, submitted for publication, 1994.","DOI":"10.1007\/3-540-58179-0_63"},{"key":"15_CR8","doi-asserted-by":"crossref","unstructured":"O. Grumberg and D.E. Long, \u201cModel Checking and Modular Verification\u201d, in: LNCS 527, 1991.","DOI":"10.1007\/3-540-54430-5_93"},{"key":"15_CR9","unstructured":"R.P. Kurshan, \u201cReducibility in Analysis of Coordination\u201d, in: LNCS 103, 1987."},{"key":"15_CR10","unstructured":"D.E. Long, \u201cModel Checking, Abstraction and Compositional Verification\u201d, Ph.D. Thesis, CMU, 1993."},{"key":"15_CR11","doi-asserted-by":"crossref","unstructured":"K.L. McMillan, \u201cSymbolic Model Checking\u201d, Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"15_CR12","doi-asserted-by":"crossref","unstructured":"Z. Manna and A. Pnueli, \u201cThe Temporal Logic of Reactive and Concurrent Systems; Specification\u201d, Springer-Verlag, 1991.","DOI":"10.1007\/978-1-4612-0931-7"},{"key":"15_CR13","unstructured":"\u201cPCI Local Bus Specification, Revision 2.0\u201d, PCI Special Interest Group, 1993."},{"key":"15_CR14","doi-asserted-by":"crossref","unstructured":"A. Pnueli, \u201cApplications of Temporal Logic to the Specification and Verification of Recative Systems: A Survey of Current Trends\u201d, in: Current Trends in Concurrency, J.W.de Bakker et al., eds., LNCS 224, 1986.","DOI":"10.1007\/BFb0027047"},{"key":"15_CR15","unstructured":"G. Shurek and O. Grumberg, \u201cThe modular Framework of Computer-Aided Verification: Motivation, Solutions and Evaluation Criteria\u201d, CAV90."}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-58179-0_53.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:17:53Z","timestamp":1605647873000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-58179-0_53"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540581796","9783540484691"],"references-count":15,"URL":"https:\/\/doi.org\/10.1007\/3-540-58179-0_53","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[1994]]}}}