{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,15]],"date-time":"2025-08-15T00:28:57Z","timestamp":1755217737136,"version":"3.43.0"},"reference-count":17,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2002,11,1]],"date-time":"2002-11-01T00:00:00Z","timestamp":1036108800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Formal Methods in System Design"],"published-print":{"date-parts":[[2002,11]]},"DOI":"10.1023\/a:1020373206491","type":"journal-article","created":{"date-parts":[[2003,3,15]],"date-time":"2003-03-15T08:44:30Z","timestamp":1047717870000},"page":"317-338","source":"Crossref","is-referenced-by-count":18,"title":["A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits"],"prefix":"10.1007","volume":"21","author":[{"given":"Tamir","family":"Heyman","sequence":"first","affiliation":[]},{"given":"Danny","family":"Geist","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"5099179_CR1","doi-asserted-by":"crossref","unstructured":"P. Arunachalam and H. Oregon, \u201cDistributed binary decision diagrams for verification of large circuits,\u201d in Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Society Press, 1996, pp. 365-370.","DOI":"10.1109\/ICCD.1996.563580"},{"key":"5099179_CR2","unstructured":"S. Basonov, \u201cParallel implementation of BDD on DSM systems,\u201d M.Sc. Thesis, Computer Science Department, Technion, 1998."},{"key":"5099179_CR3","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver, \u201cRulebase: An industry-oriented formal verification tool,\u201d in 33rd Design Automation Conference, 1996, pp. 655-660.","DOI":"10.1109\/DAC.1996.545656"},{"key":"5099179_CR4","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Proc. of the 10th International Conference on Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver, \u201cOn-the-fly model checking of RCTL formulas,\u201d in Proc. of the 10th International Conference on Computer Aided Verification, LNCS, Vol. 818, Springer-Verlag, Berlin, 1998, pp. 184-194."},{"key":"5099179_CR5","doi-asserted-by":"crossref","unstructured":"A.D. Birrell and B.J. Nelson, \u201cImplementing remote procedure calls,\u201d in Proceedings of the ACM Symposium on Operating System Principles, Bretton Woods, NH, 1983, p. 3. Association for Computing Machinery.","DOI":"10.1145\/800217.806609"},{"issue":"8","key":"5099179_CR6","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R.E. Bryant","year":"1986","unstructured":"R.E. Bryant, \u201cGraph-based algorithms for boolean function manipulation,\u201d IEEE Transactions on Computers, Vol. C-35, No. 8, pp. 677-691, 1986.","journal-title":"IEEE Transactions on Computers"},{"issue":"5","key":"5099179_CR7","doi-asserted-by":"crossref","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G. Cabodi","year":"1999","unstructured":"G. Cabodi, P. Camurati, and S. Quer, \u201cImproving the efficient of BDD-based operators by means of partitioning,\u201d IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 18, No. 5, pp. 545-556, 1999.","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"},{"key":"5099179_CR8","first-page":"354","volume-title":"Proceedings of the IEEE International Conference on Computer Aided Design","author":"G. Cabodi","year":"1996","unstructured":"G. Cabodi, P. Camurati, and S. Quer, \u201cImproved reachability analysis of large FSM,\u201d in Proceedings of the IEEE International Conference on Computer Aided Design, IEEE Computer Society Press, Los Alamitos, CA, 1996, pp. 354-360."},{"key":"5099179_CR9","first-page":"23","volume-title":"Workshop on Computer Aided Verification, DIMACS, LNCS","author":"O. Coudert","year":"1990","unstructured":"O. Coudert, J.C. Madre, and C. Berthet, \u201cVerifying temporal properties of sequential machines without building their state diagrams,\u201d in R. Kurshan and E.M. Clarke (Eds.), Workshop on Computer Aided Verification, DIMACS, LNCS, Vol. 531, Springer-Verlag, New Brunswick, NJ, 1990, pp. 23-32."},{"key":"5099179_CR10","doi-asserted-by":"crossref","unstructured":"R. Fraer, G. Kamhi, B. Ziv, M.Y. Vardi, and L. Fix, \u201cPrioritized traversal: Efficient reachability analysis for verification and falsification,\u201d in Proc. of the 12th International Conference on Computer Aided Verification, Springer-Verlag, 2000.","DOI":"10.1007\/10722167_30"},{"key":"5099179_CR11","unstructured":"J. Jain, J. Bitner, J.A. Abraham, and D.S. Fussel, \u201cFunctional partitioning for verification and related problems,\u201d in Proc. Brown\/MIT VLSI Conference, 1992, pp. 210-226."},{"key":"5099179_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-3190-6","volume-title":"Symbolic Model Checking: An Approach to the State Explosion Problem","author":"K.L. McMillan","year":"1993","unstructured":"K.L. McMillan, Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, New York, 1993."},{"key":"5099179_CR13","first-page":"388","volume-title":"Proceedings of the IEEE International Conference on Computer Aided Design","author":"A. Narayan","year":"1997","unstructured":"A. Narayan, A. Isles, J. Jain, R. Brayton, and A.L. Sangiovanni-Vincentelli, \u201cReachability analysis using partitioned-ROBDDs,\u201d in Proceedings of the IEEE International Conference on Computer Aided Design, IEEE Computer Society Press, Los Alamitos, CA, 1997, pp. 388-393."},{"key":"5099179_CR14","first-page":"547","volume-title":"Proceedings of the IEEE International Conference on Computer Aided Design","author":"A. Narayan","year":"1996","unstructured":"A. Narayan, J. Jain, M. Fujita, and A.L. Sangiovanni-Vincentelli, \u201cPartitioned-ROBDDs,\u201d in Proceedings of the IEEE International Conference on Computer Aided Design, IEEE Computer Society Press, Los Alamitos, CA, 1996, pp. 547-554."},{"key":"5099179_CR15","first-page":"358","volume-title":"Proceedings of the IEEE International Conference on Computer Design","author":"R.K. Ranjan","year":"1996","unstructured":"R.K. Ranjan, J.V. Sanghavi, R.K. Brayton, and A. Sangiovanni-Vincentelli, \u201cBinary decision diagrams on network of workstations,\u201d in Proceedings of the IEEE International Conference on Computer Design, IEEE Computer Society Press, Los Alamitos, CA, 1996, pp. 358-364."},{"key":"5099179_CR16","series-title":"LNCS","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Proc. of the 9th International Conference on Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"U. Stern and D.L. Dill, \u201cParallelizing the murphy verifier,\u201d in Proc. of the 9th International Conference on Computer Aided Verification, LNCS, Vol. 1254, Springer-Verlag, Berlin, 1997, pp. 256-267."},{"key":"5099179_CR17","volume-title":"Implementation of an efficient parallelBDDpackage","author":"T. Stornetta","year":"1996","unstructured":"T. Stornetta and F. Brewer, \u201cImplementation of an efficient parallelBDDpackage,\u201d in 33rd Design Automation Conference, IEEE Computer Society Press, Los Alamitos, CA, 1996."}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020373206491.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1020373206491\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1020373206491.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:12:27Z","timestamp":1754421147000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1020373206491"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2002,11]]},"references-count":17,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2002,11]]}},"alternative-id":["5099179"],"URL":"https:\/\/doi.org\/10.1023\/a:1020373206491","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"type":"print","value":"0925-9856"},{"type":"electronic","value":"1572-8102"}],"subject":[],"published":{"date-parts":[[2002,11]]}}}