{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T21:08:54Z","timestamp":1725484134621},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540439288"},{"type":"electronic","value":"9783540456148"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2002]]},"DOI":"10.1007\/3-540-45614-7_9","type":"book-chapter","created":{"date-parts":[[2007,5,17]],"date-time":"2007-05-17T00:45:28Z","timestamp":1179362728000},"page":"146-162","source":"Crossref","is-referenced-by-count":4,"title":["An Algorithmic Approach to Design Exploration"],"prefix":"10.1007","author":[{"given":"Sharon","family":"Barner","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Shoham","family":"Ben-David","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anna","family":"Gringauze","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Baruch","family":"Sterin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Yaron","family":"Wolfsthal","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2002,7,9]]},"reference":[{"key":"9_CR1","series-title":"Lect Notes Comput Sci","first-page":"283","volume-title":"Proc. 3rd International Conference on Formal Methods in Computer-Aided Design (FMCAD)","author":"N. Amla","year":"2000","unstructured":"N. Amla, E.A. Emerson, R.P. Kurshan, K.S. Namjoshi. Model Checking Synchronous Timing Diagrams. In Proc. 3 rd International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS 1954, pages 283\u2013298, 2000."},{"key":"9_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"72","DOI":"10.1007\/3-540-48683-6_9","volume-title":"Proc. 11th International Conference on Computer Aided Verification (CAV)","author":"J. Baumgartner","year":"1999","unstructured":"J. Baumgartner, T. Heyman, V. Singhal, and A. Aziz. Model checking the IBM Gigahertz Processor. In Proc. 11 th International Conference on Computer Aided Verification (CAV), LNCS 1633, pages 72\u201383. Springer-Verlag, 1999."},{"key":"9_CR3","doi-asserted-by":"crossref","unstructured":"J. Baumgartner, A. Tripp, A. Aziz, V. Singhal and F. Andersen. An Abstraction Algorithm for the Verification of Generalized C-slow Designs. In Proc. of 12 th International Conference on Computer Aided Verification (CAV), 2000, pp. 5\u201319.","DOI":"10.1007\/10722167_5"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver. RuleBase: an industry-oriented formal verification tool. In Proc. 33 rd Design Automation Conference (DAC), pages 655\u2013660. Association for Computing Machinery, Inc., June 1996.","DOI":"10.1145\/240518.240642"},{"key":"9_CR5","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, A. Landver, On-The-Fly Model Checking of RCTL Formulas. In Proc. of 10 th International Conference (CAV), 1998, pp. 184\u2013194.","DOI":"10.1007\/BFb0028744"},{"key":"9_CR6","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"363","DOI":"10.1007\/3-540-44585-4_33","volume-title":"Proc. of 13th International Conference on Compute Aided verification (CAV)","author":"I. Beer","year":"2001","unstructured":"I. Beer, S. Ben-David, C. Eisner, D. Fisman, A. Gringauze, Y. Rodeh. The Temporal Logic Sugar. In Proc. of 13 th International Conference on Compute Aided verification (CAV), LNCS 2102, 2001, pp. 363\u2013367."},{"key":"9_CR7","unstructured":"S. Ben-David, A. Gringauze, B. Sterin, Y. Wolfsthal. Design Exploration Through Model Checking Technical Report H0097, IBM Haifa Research Laboratory."},{"key":"9_CR8","doi-asserted-by":"crossref","unstructured":"R.E. Bryant, Graph-based algorithms for boolean function manipulation, In IEEE Transactions on Computers, C-35(8), 1986.","DOI":"10.1109\/TC.1986.1676819"},{"key":"9_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/3-540-44798-9_23","volume-title":"Proc. Correct Hardware Design and Verification Methods (CHARME)","author":"F. Copty","year":"2001","unstructured":"F. Copty, A. Irron, O. Weissberg, N. Kropp, G. Kamhi. Efficient Debugging in a Formal Verification Environment In Proc. Correct Hardware Design and Verification Methods (CHARME), LNCS 2144, page 275\u2013292, 2001."},{"key":"9_CR10","unstructured":"G.F. De Palma, A.B. Glaser, R.P. Kurshan, G.R. Wesley, Apparatus for defining Properties in Finite-State Machines. US Patent 6,966,516, October 1999."},{"key":"9_CR11","series-title":"Lect Notes Comput Sci","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/3-540-49519-3_5","volume-title":"Second International Conference on Formal Methods in Computer-Aided Design (FMCAD)","author":"Eir\u00edksson","year":"1998","unstructured":"\u00c1. Eir\u00edksson. The formal design of 1M-gate ASICs. In Second International Conference on Formal Methods in Computer-Aided Design (FMCAD), LNCS 1522, pages 49\u201363. Springer-Verlag, 1998."},{"key":"9_CR12","doi-asserted-by":"crossref","unstructured":"C. Eisner, R. Hoover, W. Nation, K. Nelson, I. Shitsevalov, and K. Valk. A methodology for formal design of hardware control with application to cache coherence protocols. In Proc. 37 th Design Automation Conference (DAC), pages 724\u2013729. Association for Computing Machinery, Inc., June 2000.","DOI":"10.1145\/337292.337757"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"K. Fisler Timing Diagrams: Formalization and Formal Verification, In Journal of Logic, Language and Information 8(3), 1999.","DOI":"10.1023\/A:1008345113376"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"A. Goel and W. Lee. Formal verification of an IBM Coreconnect Processor Local Bus arbiter core. In Proc. 37 th Design Automation Conference (DAC), pages 196\u2013200. Association for Computing Machinery, Inc., June 2000.","DOI":"10.1145\/337292.337384"},{"key":"9_CR15","doi-asserted-by":"crossref","unstructured":"E. Gunter and D. Peled. Temporal Debugging for Concurrent Systems. To appear in TACAS 2002","DOI":"10.1007\/3-540-46002-0_30"},{"key":"9_CR16","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Proc. of 8th International Conference on Computer Aided Verification (CAV)","author":"H. Hardin","year":"1996","unstructured":"H. Hardin, Z. Har\u2019El, R.P. Kurshan. COSPAN. In Proc. of 8 th International Conference on Computer Aided Verification (CAV), LNCS 1102, 1996, pp. 423\u2013427."},{"key":"9_CR17","unstructured":"P. Interest PCI Local Bus Specification, PCI Special Interest group, PCI Local Bus Specification, Revision 2.2, December 1995."},{"key":"9_CR18","unstructured":"D. Long. Model Checking, Abstraction and Compositional Verification. Ph.D. Thesis, CMU, 1993."},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"K.L. McMillan. Symbolic Model Checking. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"issue":"1\u20133","key":"9_CR20","first-page":"278","volume":"37","author":"K.L. McMillan","year":"2000","unstructured":"K.L. McMillan. A Methodology for Hardware Verification using Compositional Model-Checking. In Science of Computer Programming, 37(1\u20133):278\u2013309 (2000)","journal-title":"Science of Computer Programming"},{"key":"9_CR21","doi-asserted-by":"crossref","unstructured":"K. Ravi, F. Somenzi. Hints to Accelerate Symbolic Traversal. In Proc of CHARME, 1999, pp. 250\u2013264.","DOI":"10.1007\/3-540-48153-2_19"},{"key":"9_CR22","unstructured":"I. SM and T. Association. InfiniBand Architecture Specification. InfiniBand(SM) Trade Association, InfiniBand Architecture Specification, Release 1.0 October 2000. Available from: http:\/\/www.infinibandta.org ."},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"B.D. Winters, A.J. Hu. Source-Level Transformations for Improved Formal Verification. In IEEE International Conference on Computer Design, 2000.","DOI":"10.1109\/ICCD.2000.878353"}],"container-title":["Lecture Notes in Computer Science","FME 2002:Formal Methods\u2014Getting IT Right"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-45614-7_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,28]],"date-time":"2019-04-28T00:05:32Z","timestamp":1556409932000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-45614-7_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002]]},"ISBN":["9783540439288","9783540456148"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/3-540-45614-7_9","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2002]]}}}