{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T15:27:50Z","timestamp":1725550070828},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540292098"},{"type":"electronic","value":"9783540319696"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11562948_5","type":"book-chapter","created":{"date-parts":[[2005,10,10]],"date-time":"2005-10-10T14:06:40Z","timestamp":1128953200000},"page":"26-38","source":"Crossref","is-referenced-by-count":1,"title":["A New Reachability Algorithm for Symmetric Multi-processor Architecture"],"prefix":"10.1007","author":[{"given":"Debashis","family":"Sahoo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jawahar","family":"Jain","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Subramanian","family":"Iyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"David","family":"Dill","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"unstructured":"Clarke, E., Emerson, E.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Logic of Programs 1981. LNCS, vol.\u00a0131. Springer, Heidelberg (1981)","key":"5_CR1"},{"key":"5_CR2","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking","author":"K.L. McMillan","year":"1993","unstructured":"McMillan, K.L.: Symbolic Model Checking. Kluwer Academic Publishers, Dordrecht (1993)"},{"key":"5_CR3","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. Bryant","year":"1986","unstructured":"Bryant, R.: Graph-based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers\u00a0C-35, 677\u2013691 (1986)","journal-title":"IEEE Transactions on Computers"},{"doi-asserted-by":"crossref","unstructured":"Coudert, O., Berthet, C., Madre, J.C.: Verification of sequential machines based on symbolic execution. In: Proc. of the Workshop on Automatic Verification Methods for Finite State Systems (1989)","key":"5_CR4","DOI":"10.1007\/3-540-52148-8_30"},{"unstructured":"Jain, J., et al.: Functional Partitioning for Verification and Related Problems. In: Brown\/MIT VLSI Conference (1992)","key":"5_CR5"},{"doi-asserted-by":"crossref","unstructured":"Narayan, A., et al.: Reachability Analysis Using Partitioned-ROBDDs. In: ICCAD, pp. 388\u2013393 (1997)","key":"5_CR6","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"5_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-540-39724-3_35","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Iyer","year":"2003","unstructured":"Iyer, S., Sahoo, D., Stangier, C., Narayan, A., Jain, J.: Improved symbolic Verification Using Partitioning Techniques. In: Geist, D., Tronci, E. (eds.) CHARME 2003. LNCS, vol.\u00a02860, pp. 410\u2013424. Springer, Heidelberg (2003)"},{"key":"5_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"399","DOI":"10.1007\/978-3-540-30494-4_28","volume-title":"Formal Methods in Computer-Aided Design","author":"D. Sahoo","year":"2004","unstructured":"Sahoo, D., Iyer, S., et al.: A Partitioning Methodology for BDD-based Verification. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 399\u2013413. Springer, Heidelberg (2004)"},{"doi-asserted-by":"crossref","unstructured":"Stern, U., Dill, D.L.: Parallelizing the murphy verifier. In: CAV (1997)","key":"5_CR9","DOI":"10.1007\/3-540-63166-6_26"},{"doi-asserted-by":"crossref","unstructured":"Stornetta, T., Brewer, F.: Implementation of an efficient parallel BDD package. In: DAC, pp. 641\u2013644 (1996)","key":"5_CR10","DOI":"10.1145\/240518.240639"},{"key":"5_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1007\/3-540-45139-0_14","volume-title":"Model Checking Software","author":"H. Garavel","year":"2001","unstructured":"Garavel, H., Mateescu, R., Smarandache, I.: Parallel state space construction for model-checking. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 217\u2013234. Springer, Heidelberg (2001)"},{"doi-asserted-by":"crossref","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: Achieving scalability in parallel reachability analysis of very large circuits. In: CAV (2000)","key":"5_CR12","DOI":"10.1007\/10722167_6"},{"key":"5_CR13","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1145\/263764.263784","volume-title":"Symposium on Principles and practice of parallel programming","author":"B. Yang","year":"1997","unstructured":"Yang, B., O\u2019Hallaron, D.R.: Parallel breadth-first bdd construction. In: Symposium on Principles and practice of parallel programming, pp. 145\u2013156. ACM Press, New York (1997)"},{"doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Lavagno, L., Quer, S.: Disjunctive partitioning and partial iterative squaring: An effective approach for symbolic traversal of large circuits. In: DAC, pp. 728\u2013733 (1997)","key":"5_CR14","DOI":"10.1145\/266021.266355"},{"unstructured":"Pixley, C., Havlicek, J.: A verification synergy: Constraint-based verification. In: Electronic Design Processes (2003)","key":"5_CR15"},{"doi-asserted-by":"crossref","unstructured":"Sahoo, D., Jain, J., Iyer, S.K., Dill, D.L., Emerson, E.A.: Multi-threaded reachability. In: DAC (2005) (to appear)","key":"5_CR16","DOI":"10.1145\/1065579.1065701"},{"doi-asserted-by":"crossref","unstructured":"Ravi, K., Somenzi, F.: High-density reachability analysis. In: ICCAD, pp. 154\u2013158 (1995)","key":"5_CR17","DOI":"10.1109\/ICCAD.1995.480006"},{"unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package (2001), ftp:\/\/vlsi.colorado.edu\/pub","key":"5_CR18"},{"unstructured":"VIS: Verilog Benchmarks (2001), http:\/\/vlsi.colorado.edu\/~vis\/","key":"5_CR19"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11562948_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T19:52:21Z","timestamp":1605642741000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11562948_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540292098","9783540319696"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/11562948_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}