{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,10,22]],"date-time":"2024-10-22T15:02:01Z","timestamp":1729609321862,"version":"3.28.0"},"reference-count":29,"publisher":"IEEE","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2006]]},"DOI":"10.1109\/ipdps.2006.1639371","type":"proceedings-article","created":{"date-parts":[[2006,7,10]],"date-time":"2006-07-10T19:59:56Z","timestamp":1152561596000},"page":"10 pp.","source":"Crossref","is-referenced-by-count":2,"title":["A dynamic firing speculation to speedup distributed symbolic state-space generation"],"prefix":"10.1109","author":[{"family":"Ming-Ying Chung","sequence":"first","affiliation":[]},{"given":"G.","family":"Ciardo","sequence":"additional","affiliation":[]}],"member":"263","reference":[{"key":"19","first-page":"501","article-title":"A parallel BDD package","author":"milvang-jensen","year":"1998","journal-title":"Proc FMCAD"},{"key":"17","first-page":"9","article-title":"Multi-valued decision diagrams: Theory and applications","volume":"4","author":"kam","year":"1998","journal-title":"Multiple-Valued Logic"},{"key":"18","doi-asserted-by":"publisher","DOI":"10.1109\/ICCD.1990.130209"},{"key":"15","first-page":"54","article-title":"A work-efficient distributed algorithm for reachability analysis","author":"grumberg","year":"2003","journal-title":"Proc CAV"},{"year":"0","key":"16"},{"key":"13","doi-asserted-by":"publisher","DOI":"10.1109\/FMPC.1995.380467"},{"key":"14","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211911"},{"key":"11","article-title":"Logical and stochastic modeling with SMART","author":"ciardo","year":"0","journal-title":"Performance Evaluation"},{"journal-title":"Model checking","year":"1999","author":"clarke","key":"12"},{"key":"21","first-page":"388","author":"narayan","year":"1997","journal-title":"Reachability analysis using Partitioned-ROBDDs Proc"},{"key":"20","first-page":"6","article-title":"Efficient reachability set generation and storage using decision diagrams","author":"miner","year":"1999","journal-title":"Proc ICATPN"},{"key":"22","doi-asserted-by":"crossref","first-page":"153","DOI":"10.1006\/jpdc.1997.1409","article-title":"Automated parallelization of discrete state-space generation","volume":"47","author":"nicol","year":"1997","journal-title":"J Parall Distrib Comp"},{"key":"23","first-page":"16","article-title":"Parallel implementation of BDD algorithm using a distributed shared memory. Proc","author":"parasuram","year":"1994","journal-title":"HICSS"},{"key":"24","first-page":"416","article-title":"Petri net analysis using boolean manipulation","author":"pastor","year":"1994","journal-title":"Proc ICATPN"},{"key":"25","first-page":"356","article-title":"Binary decision diagrams on network of workstations. Proc","author":"ranjan","year":"1996","journal-title":"ICCD"},{"key":"26","article-title":"Formal verification of the NASA Runway Safety Monitor. Proc","author":"siminiceanu","year":"2004","journal-title":"AVoCS"},{"key":"27","first-page":"256","article-title":"Parallelizing the Mur\ufffd verifier","author":"stern","year":"1997","journal-title":"Proc CAV"},{"key":"28","doi-asserted-by":"publisher","DOI":"10.1145\/240518.240639"},{"key":"29","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1145\/263764.263784","article-title":"Parallel breadth-first BDD construction","author":"yang","year":"1997","journal-title":"Proceedings of PPoPP"},{"key":"3","doi-asserted-by":"publisher","DOI":"10.1287\/ijoc.12.3.203.12634"},{"key":"2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.1986.1676819"},{"year":"0","key":"10"},{"key":"1","doi-asserted-by":"crossref","first-page":"43","DOI":"10.1007\/s10009-003-0129-2","article-title":"Sequential and distributed model checking of Petri nets","volume":"7","author":"bell","year":"2005","journal-title":"STTT"},{"key":"7","first-page":"103","article-title":"Efficient symbolic state-space construction for asynchronous systems","author":"ciardo","year":"2000","journal-title":"Proc ICATPN"},{"key":"6","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.019"},{"key":"5","first-page":"272","author":"chung","year":"2004","journal-title":"Saturation NOW Proc"},{"key":"4","first-page":"49","article-title":"Symbolic model checking with partitioned transition relations. Proc","author":"burch","year":"1991","journal-title":"VLSI"},{"key":"9","first-page":"379","article-title":"Saturation unbound","author":"ciardo","year":"2003","journal-title":"Proc TACAS"},{"key":"8","first-page":"328","article-title":"Saturation: An efficient iteration strategy for symbolic state-space generation","author":"ciardo","year":"2001","journal-title":"Proc TACAS"}],"event":{"name":"Proceedings 20th IEEE International Parallel & Distributed Processing Symposium","start":{"date-parts":[[2006,4,25]]},"location":"Rhodes Island, Greece","end":{"date-parts":[[2006,4,29]]}},"container-title":["Proceedings 20th IEEE International Parallel & Distributed Processing Symposium"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx5\/10917\/34366\/01639371.pdf?arnumber=1639371","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2017,6,17]],"date-time":"2017-06-17T07:22:58Z","timestamp":1497684178000},"score":1,"resource":{"primary":{"URL":"http:\/\/ieeexplore.ieee.org\/document\/1639371\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006]]},"references-count":29,"URL":"https:\/\/doi.org\/10.1109\/ipdps.2006.1639371","relation":{},"subject":[],"published":{"date-parts":[[2006]]}}}