{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T15:08:27Z","timestamp":1758121707109,"version":"3.33.0"},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540412199"},{"type":"electronic","value":"9783540409229"}],"license":[{"start":{"date-parts":[[2000,1,1]],"date-time":"2000-01-01T00:00:00Z","timestamp":946684800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-40922-x_24","type":"book-chapter","created":{"date-parts":[[2007,11,29]],"date-time":"2007-11-29T09:41:36Z","timestamp":1196329296000},"page":"427-441","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["Scalable Distributed On-the-Fly Symbolic Model Checking"],"prefix":"10.1007","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2002,6,18]]},"reference":[{"key":"24_CR1","doi-asserted-by":"crossref","unstructured":"I. Beer, S. Ben-David, C. Eisner, and A. Landver. Rulebase: An Industry-Oriented Formal Verification Tool. In 33rd Design Automation Conference, pages 655\u2013660, 1996.","DOI":"10.1145\/240518.240642"},{"key":"24_CR2","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"184","DOI":"10.1007\/BFb0028744","volume-title":"On-The-Fly Model Checking of RCTL Formulas","author":"I. Beer","year":"1998","unstructured":"I. Beer, S. Ben-David, and A. Landver. On-The-Fly Model Checking of RCTL Formulas. In Proc. of the 10th International Conference on Computer Aided Verification, LNCS 818, pages 184\u2013194. Springer-Verlag, June\u2013July 1998."},{"key":"24_CR3","unstructured":"G. Bhat, R. Cleaveland, and O. Grumberg. Efficient On-The-Fly Model Checking for CTL*. In Proc. of the Conference on Logic in Computer Science (LICS\u201995), June 1995."},{"issue":"8","key":"24_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C-35","author":"R. E. Bryant","year":"1986","unstructured":"R. E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"24_CR5","unstructured":"J. R. Burch, E. M. Clarke, and D. E. Long. Symbolic model checking with partitioned transition relations. In A. Halaas and P. B. Denyer, editors, Proceedings of the 1991 International Conference on Very Large Scale Integration, August 1991. Winner of the SidneyMichaelson Best Paper Award."},{"issue":"2","key":"24_CR6","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"J. R. Burch","year":"1992","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142\u2013170, June 1992.","journal-title":"Information and Computation"},{"key":"24_CR7","doi-asserted-by":"crossref","unstructured":"Gianpiero Cabodi, Paolo Camurati, and Stefano Que. Improved Reachability Analysis of Large FSM. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 354\u2013360. IEEE Computer Society Press, June 1996.","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"24_CR8","doi-asserted-by":"crossref","unstructured":"E. Clarke, O. Grumberg, K. McMillan, and X. Zhao. Efficient Generation of Counterexamples and Witnesses in Symbolic Model Checking. In 32rd Design Automation Conference, pages 655\u2013660, 1995.","DOI":"10.1109\/DAC.1995.249985"},{"key":"24_CR9","series-title":"Lect Notes Comput Sci","first-page":"23","volume-title":"Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams","author":"O. Coudert","year":"1990","unstructured":"Olivier Coudert, Jean C. Madre, and Christian Berthet. Verifying Temporal Properties of Sequential Machines Without Building their State Diagrams. In R. Kurshan and E. M. Clarke, editors, Workshop on Computer Aided Verification, DIMACS, LNCS 531, pages 23\u201332. Springer-Verlag, New Brunswick, NJ, June 1990."},{"key":"24_CR10","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C. Courcoubetis","year":"1992","unstructured":"C. Courcoubetis, M. Vardi, P. Wolper, and M. Yannakakis. Memory efficient algorithms for the verification of temporal properties. Formal Methods in System Design, 1:275\u2013288, 1992.","journal-title":"Formal Methods in System Design"},{"key":"24_CR11","doi-asserted-by":"crossref","unstructured":"T. Heyman, D. Geist, O. Grumberg, and A. Schuster. Achieving scalability in parallel reachability analysis of very large circuits. In Proc. of the 12th International Conference on Computer Aided Verification. Springer-Verlag, June 2000.","DOI":"10.1007\/10722167_6"},{"key":"24_CR12","unstructured":"J. E. Hopcroft and J. Ullman. Introduction to Automata Theory, Languages and Computation. Addison Wesely Pub. Co, 1979."},{"key":"24_CR13","unstructured":"D. E. Long. Model Checking, Abstraction, and Compositional Reasoning. PhD thesis, Carnegie Mellon University, 1993."},{"key":"24_CR14","doi-asserted-by":"crossref","unstructured":"K. L. McMillan. Symbolic Model Checking: An Approach to the State Explosion Problem. Kluwer Academic Publishers, 1993.","DOI":"10.1007\/978-1-4615-3190-6"},{"key":"24_CR15","doi-asserted-by":"crossref","unstructured":"Adrian A. Narayan, Jain J. Jawahar Isles, Robert K. Brayton, and Alberto L. Sangiovanni-Vincentelli. Reachability Analysis Using Partitioned-ROBDDs. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 388\u2013393. IEEE Computer Society Press, June 1997.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"24_CR16","unstructured":"Adrian A. Narayan, Jain Jawahar, M. Fujita, and A. Sangiovanni-Vincentelli. Partitioned-ROBDDs. In Proceedings of the IEEE International Conference on Computer Aided Design, pages 547\u2013554. IEEE Computer Society Press, June 1996."},{"key":"24_CR17","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"377","DOI":"10.1007\/3-540-58179-0_69","volume-title":"Combining Partial Order Reductions with On-The-Fly Model Checking","author":"D. Peled","year":"1994","unstructured":"Doron Peled. Combining Partial Order Reductions with On-The-Fly Model Checking. In Proc. of the Sixth International Conference on Computer Aided Verification, LNCS 818, pages 377\u2013390. Springer-Verlag, June 1994."},{"key":"24_CR18","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"256","DOI":"10.1007\/3-540-63166-6_26","volume-title":"Parallelizing the Murphy Verifier","author":"U. Stern","year":"1997","unstructured":"Ulrich Stern and David L. Dill. Parallelizing the Murphy Verifier. In Proc. of the 9th International Conference on Computer Aided Verification, LNCS 1254, pages 256\u2013267. Springer-Verlag, June 1997."}],"container-title":["Lecture Notes in Computer Science","Formal Methods in Computer-Aided Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-40922-X_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,23]],"date-time":"2025-01-23T00:22:55Z","timestamp":1737591775000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-40922-X_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540412199","9783540409229"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/3-540-40922-x_24","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]},"assertion":[{"value":"18 June 2002","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}