{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T20:10:21Z","timestamp":1736021421338,"version":"3.32.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540291053"},{"type":"electronic","value":"9783540320302"}],"license":[{"start":{"date-parts":[[2005,1,1]],"date-time":"2005-01-01T00:00:00Z","timestamp":1104537600000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2005]]},"DOI":"10.1007\/11560548_12","type":"book-chapter","created":{"date-parts":[[2005,10,6]],"date-time":"2005-10-06T09:38:22Z","timestamp":1128591502000},"page":"129-145","source":"Crossref","is-referenced-by-count":27,"title":["Achieving Speedups in Distributed Symbolic Reachability Analysis Through Asynchronous Computation"],"prefix":"10.1007","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Nili","family":"Ifergan","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"200","DOI":"10.1007\/3-540-45139-0_13","volume-title":"Model Checking Software","author":"J. Barnat","year":"2001","unstructured":"Barnat, J., Brim, L., Stribrna, J.: Distributed LTL model-checking in SPIN. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol.\u00a02057, pp. 200\u2013216. Springer, Heidelberg (2001)"},{"key":"12_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"Computer Aided Verification","author":"I. Beer","year":"1998","unstructured":"Beer, I., Ben-David, S., Landver, A.: On-The-Fly Model Checking of RCTL Formulas. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol.\u00a01427, pp. 184\u2013194. Springer, Heidelberg (1998)"},{"key":"12_CR3","series-title":"Electronic Notes in Theoretical Computer Science","volume-title":"Proceedings of the 7th International ERCIM Workshop, FMICS 2002","author":"A. Biere","year":"2002","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness Checking as Safety Checking. In: Proceedings of the 7th International ERCIM Workshop, FMICS 2002. Electronic Notes in Theoretical Computer Science, vol.\u00a066(2). Elsevier, Amsterdam (2002)"},{"key":"12_CR4","series-title":"Advances in Computers","volume-title":"Bounded Model Checking","author":"A. Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zue, Y.: Bounded Model Checking. Advances in Computers, vol.\u00a058. Academic Press, London (2003)"},{"issue":"1","key":"12_CR5","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/s10009-004-0143-z","volume":"7","author":"V.A. Braberman","year":"2005","unstructured":"Braberman, V.A., Olivero, A., Schapachnik, F.: Issues in distributed timed model checking: Building Zeus. STTT\u00a07(1), 4\u201318 (2005)","journal-title":"STTT"},{"key":"12_CR6","unstructured":"Burch, J.R., Clarke, E.M., Long, D.E.: Symbolic Model Checking with Partitioned Transition Relations. In: Proceedings of Internation Conference on Very Large Integration, pp. 45\u201358 (1991)"},{"key":"12_CR7","doi-asserted-by":"crossref","unstructured":"Cabodi, G., Camurati, P., Quer, S.: Improved Reachability Analysis of Large FSM. In: Proceedings of the IEEE International Conference on CAD, pp. 354\u2013360 (1996)","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"12_CR8","unstructured":"Chauhan, P., Clarke, E.M., Kroening, D.: Using SAT based Image Computation for Reachability Analysis. Technical report, Carnegie Mellon University, School of Computer Science (2003)"},{"key":"12_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/3-540-48683-6_44","volume-title":"Computer Aided Verification","author":"A. Cimatti","year":"1999","unstructured":"Cimatti, A., Clarke, E.M., Giunchiglia, F., Roveri, M.: NuSMV: a new Symbolic Model Verifier. In: Halbwachs, N., Peled, D.A. (eds.) CAV 1999. LNCS, vol.\u00a01633, pp. 495\u2013499. Springer, Heidelberg (1999)"},{"key":"12_CR10","volume-title":"Model checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model checking. MIT Press, Cambridge (1999)"},{"key":"12_CR11","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Feijen, W.H.J., van Gasteren, A.J.M.: Derivation of a Termination Detection Algorithm for Distributed Computations. Information Processing Letters, 217\u2013219 (1983)","DOI":"10.1016\/0020-0190(83)90092-3"},{"key":"12_CR12","doi-asserted-by":"crossref","unstructured":"Dijkstra, E.W., Scholten, C.S.: Termination Detection for Diffusing Computations. Information Processing Letters, 1\u20134 (1980)","DOI":"10.1016\/0020-0190(80)90021-6"},{"key":"12_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_30","volume-title":"Computer Aided Verification","author":"R. Fraer","year":"2000","unstructured":"Fraer, R., Kamhi, G., Barukh, Z., Vardi, M.Y., Fix, L.: Prioritized Traversal: Efficient Reachability Analysis for Verification and Falsification. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"12_CR14","unstructured":"Grumberg, O., Heyman, A., Heyman, T., Schuster, A.: Division System: A General Platform for Distributed Symbolic Model Checking Research (2003)"},{"key":"12_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/978-3-540-45069-6_5","volume-title":"Computer Aided Verification","author":"O. Grumberg","year":"2003","unstructured":"Grumberg, O., Heyman, T., Schuster, A.: A Work-Efficient Distributed Algorithm for Reachability Analysis. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 54\u201366. Springer, Heidelberg (2003)"},{"key":"12_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory Efficient All-Solutions SAT Solver and its Application for Reachability Analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 275\u2013289. Springer, Heidelberg (2004)"},{"key":"12_CR17","first-page":"536","volume-title":"DAC","author":"A. Gupta","year":"2001","unstructured":"Gupta, A., Gupta, A., Yang, Z., Ashar, P.: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation. In: DAC, pp. 536\u2013541. ACM Press, New York (2001)"},{"key":"12_CR18","first-page":"286","volume-title":"ICCAD","author":"A. Gupta","year":"2001","unstructured":"Gupta, A., Yang, Z., Ashar, P., Zhang, L., Malik, S.: Partition-Based Decision Heuristics for Image Computation using SAT and BDDs. In: ICCAD, pp. 286\u2013292. IEEE Press, Los Alamitos (2001)"},{"key":"12_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/3-540-40922-X_22","volume-title":"Formal Methods in Computer-Aided Design","author":"A. Gupta","year":"2000","unstructured":"Gupta, A., Yang, Z., Ashar, P., Gupta, A.: SAT-Based Image Computation with Application in Reachability Analysis. In: Johnson, S.D., Hunt Jr., W.A. (eds.) FMCAD 2000. LNCS, vol.\u00a01954, pp. 354\u2013371. Springer, Heidelberg (2000)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Heyman, T., Geist, D., Grumberg, O., Schuster, A.: A Scalable Parallel Algorithm for Reachability Analysis of Very Large Circuits. Formal Methods in System Design, 317\u2013338 (2002)","DOI":"10.1023\/A:1020373206491"},{"key":"12_CR21","doi-asserted-by":"crossref","unstructured":"Kang, H., Park, I.: SAT-based Unbounded Symbolic Model Checking. In: DAC (2003)","DOI":"10.1145\/776038.776043"},{"key":"12_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"22","DOI":"10.1007\/3-540-48234-2_3","volume-title":"Theoretical and Practical Aspects of SPIN Model Checking","author":"F. Lerda","year":"1999","unstructured":"Lerda, F., Sisto, R.: Distributed-Memory Model Checking with SPIN. In: Dams, D.R., Gerth, R., Leue, S., Massink, M. (eds.) SPIN 1999. LNCS, vol.\u00a01680, pp. 22\u201339. Springer, Heidelberg (1999)"},{"key":"12_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/10722167_25","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2000","unstructured":"McMillan, K.L.: Applying SAT Methods in Unbounded Symbolic Model Checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855. Springer, Heidelberg (2000)"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/3-540-49519-3_32","volume-title":"Formal Methods in Computer-Aided Design","author":"K. Milvang-Jensen","year":"1998","unstructured":"Milvang-Jensen, K., Hu, A.J.: BDDNOW: A Parallel BDD Package. In: Gopalakrishnan, G.C., Windley, P. (eds.) FMCAD 1998. LNCS, vol.\u00a01522, pp. 501\u2013507. Springer, Heidelberg (1998)"},{"key":"12_CR25","doi-asserted-by":"crossref","unstructured":"Narayan, A., Isles, A., Jain, J., Brayton, R., Sangiovanni-Vincentelli, A.L.: Reachability Analysis Using Partitioned-ROBDDs. In: Proceedings of the IEEE International Conference on Computer Aided Design, pp. 388\u2013393 (1997)","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","first-page":"547","volume-title":"Computer Aided Verification","author":"A.A. Narayan","year":"1996","unstructured":"Narayan, A.A., Jawahar, J., Fujita, M., Sangiovanni-Vincenteli, A.: Partitioned-ROBDDs. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 547\u2013554. Springer, Heidelberg (1996)"},{"issue":"2","key":"12_CR27","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1006\/jpdc.1997.1409","volume":"47","author":"D.M. Nicol","year":"1997","unstructured":"Nicol, D.M., Ciardo, G.: Automated Parallelization of Discrete State-Space Generation. J. Parallel Distrib. Comput.\u00a047(2), 153\u2013167 (1997)","journal-title":"J. Parallel Distrib. Comput."},{"key":"12_CR28","doi-asserted-by":"crossref","unstructured":"Prasad, M.R., Biere, A., Gupta, A.: A Survey of Recent Advances in SAT-Based Verification. To appear in STTT 2005 (2005)","DOI":"10.1007\/s10009-004-0183-4"},{"key":"12_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Computer Aided Verification","author":"U. Stern","year":"1997","unstructured":"Stern, U., Dill, D.L.: Parallelizing the Mur\u03d5 Verifier. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 256\u2013278. Springer, Heidelberg (1997)"},{"key":"12_CR30","doi-asserted-by":"crossref","unstructured":"Stornetta, T., Brewer, F.: Implementation of an Efficient Parallel BDD Package. In: 33rd Design Automation Conference (1996)","DOI":"10.1145\/240518.240639"}],"container-title":["Lecture Notes in Computer Science","Correct Hardware Design and Verification Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/11560548_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,4]],"date-time":"2025-01-04T19:51:36Z","timestamp":1736020296000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/11560548_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005]]},"ISBN":["9783540291053","9783540320302"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/11560548_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2005]]}}}