{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:25:25Z","timestamp":1761611125151,"version":"3.30.2"},"reference-count":21,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2003,8,1]],"date-time":"2003-08-01T00:00:00Z","timestamp":1059696000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["STTT"],"published-print":{"date-parts":[[2003,8]]},"DOI":"10.1007\/s10009-002-0093-2","type":"journal-article","created":{"date-parts":[[2004,3,20]],"date-time":"2004-03-20T15:13:37Z","timestamp":1079795617000},"page":"496-504","source":"Crossref","is-referenced-by-count":8,"title":["Scalable distributed on-the-fly symbolic model checking"],"prefix":"10.1007","volume":"4","author":[{"given":"Shoham","family":"Ben-David","sequence":"first","affiliation":[]},{"given":"Orna","family":"Grumberg","sequence":"additional","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2003,8,1]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Armoni R, Fix L, Flaisher A, Gerth R, Ginsburg B, Kanza T, Landver A, Mador-Haim S, Singerman E, Tiemeyer A, Vardi MY, Zbar Y: The ForSpec temporal logic: a new temporal property-specification language. In: International Conference on Tools and Algorithms for Construction and Analysis of Systems. Springer, Berlin Heidelberg New York, 2002","key":"93_CITforspec02","DOI":"10.1007\/3-540-46002-0_21"},{"doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Fisman D, Gringauze A, Rodeh Y: The temporal logic Sugar. In: Proc. 13th International Conference on Computer Aided Verification. Springer, Berlin Heidelberg New York, 2001","key":"93_CITsugar01","DOI":"10.1007\/3-540-44585-4_33"},{"doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Eisner C, Landver A: Rulebase: an industry-oriented formal verification tool. In: 33rd Design Automation Conference, 1996, pp 655\u2013660","key":"93_CITdac96","DOI":"10.1145\/240518.240642"},{"doi-asserted-by":"crossref","unstructured":"Beer I, Ben-David S, Landver A: On-the-fly model checking of RCTL formulas. In: Proc. 10th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol 818. Springer, Berlin Heidelberg New York, 1998, pp 184\u2013194","key":"93_CITcav98","DOI":"10.1007\/BFb0028744"},{"doi-asserted-by":"crossref","unstructured":"Bhat G, Cleaveland R, Grumberg O: Efficient on-the-fly model checking for CTL*. In: Proc. Conference on Logic in Computer Science (LICS\u201995), 1995","key":"93_CITBCG95","DOI":"10.1109\/LICS.1995.523273"},{"issue":"8","key":"93_CITBryant86BDD","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"-35","author":"RE Bryant","year":"1986","unstructured":"Bryant RE: Graph-based algorithms for Boolean function manipulation. IEEE Trans Comput C-35(8):677\u2013691, 1986","journal-title":"IEEE Trans Comput C"},{"unstructured":"Burch JR, Clarke EM, Long DE: Symbolic model checking with partitioned transition relations. In: Halaas A, Denyer PB (eds) Proc. 1991 International Conference on Very Large Scale Integration, 1991","key":"93_CITBurchClarkeLong91async"},{"issue":"2","key":"93_CITBurchetal92smc","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1016\/0890-5401(92)90017-A","volume":"98","author":"JR Burch","year":"1992","unstructured":"Burch JR, Clarke EM, McMillan KL, Dill DL, Hwang LJ: Symbolic model checking: 1020 states and beyond. Inf Comput 98(2):142\u2013170, 1992","journal-title":"Inf Comput"},{"doi-asserted-by":"crossref","unstructured":"Cabodi G, Camurati P, Quer S: Improved reachability analysis of large FSM. In: Proc. IEEE International Conference on Computer Aided Design. IEEE Computer, New York, 1996, pp 354\u2013360","key":"93_CITccq","DOI":"10.1109\/ICCAD.1996.569819"},{"key":"93_CITcabodi99","doi-asserted-by":"publisher","first-page":"545","DOI":"10.1109\/43.759068","volume":"18","author":"G Cabodi","year":"1999","unstructured":"Cabodi G, Camurati P, Quer S: Improving the efficiency of BDD-based operators by means of partitioning. IEEE Trans Comput Aided Des 18:545\u2013556, 1999","journal-title":"IEEE Trans Comput Aided Des"},{"doi-asserted-by":"crossref","unstructured":"Clarke E, Grumberg O, McMillan K, Zhao X: Efficient generation of counterexamples and witnesses in symbolic model checking. In: 32rd Design Automation Conference, 1995, pp 655\u2013660","key":"93_CITcg","DOI":"10.1109\/DAC.1995.249985"},{"doi-asserted-by":"crossref","unstructured":"Coudert O, Madre JC, Berthet C: Verifying temporal properties of sequential machines without building their state diagrams. In: Kurshan R, Clarke EM (eds) Workshop on Computer Aided Verification, DIMACS, Lecture Notes in Computer Science, vol 531. Springer, Berlin Heidelberg New York, 1990, pp 23\u201332","key":"93_CITcoudert","DOI":"10.1007\/BFb0023716"},{"key":"93_CITCVWY92","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/BF00121128","volume":"1","author":"C Courcoubetis","year":"1992","unstructured":"Courcoubetis C, Vardi M, Wolper P, Yannakakis M: Memory efficient algorithms for the verification of temporal properties. Formal Meth Syst Des 1:275\u2013288, 1992","journal-title":"Formal Meth Syst Des"},{"doi-asserted-by":"crossref","unstructured":"Heyman T, Geist D, Grumberg O, Schuster A: Achieving scalability in parallel reachability analysis of very large circuits. In: Proc. 12th International Conference on Computer Aided Verification. Springer, Berlin Heidelberg New York, 2000","key":"93_CITparsmv","DOI":"10.1007\/10722167_6"},{"unstructured":"Hopcroft JE, Ullman J: Introduction to automata theory, languages and computation. Addison-Wesley, Reading, Mass., USA, 1979","key":"93_CITHU79"},{"unstructured":"Long DE: Model checking, abstraction, and compositional reasoning. PhD thesis, Carnegie Mellon University, 1993","key":"93_CITlongthesis"},{"doi-asserted-by":"crossref","unstructured":"McMillan KL: Symbolic model checking: an approach to the state explosion problem. Kluwer Academic, Boston, Mass., USA, 1993","key":"93_CITMcMillan92thesis","DOI":"10.1007\/978-1-4615-3190-6"},{"doi-asserted-by":"crossref","unstructured":"Narayan A, Isles A, Jain J, Brayton R, Sangiovanni-Vincentelli AL: Reachability analysis using partitioned-ROBDDs. In: Proc. IEEE International Conference on Computer Aided Design, pp 388\u2013393. IEEE Computer, New York, 1997","key":"93_CITbrkra","DOI":"10.1109\/ICCAD.1997.643565"},{"doi-asserted-by":"crossref","unstructured":"Narayan A, Jain J, Fujita M, Sangiovanni-Vincentelli AL: Partitioned-ROBDDs. In: Proc. IEEE International Conference on Computer Aided Design, pp 547\u2013554. IEEE Computer, New York, 1996","key":"93_CITbrkpo","DOI":"10.1109\/ICCAD.1996.569909"},{"doi-asserted-by":"crossref","unstructured":"Peled D: Combining partial order reductions with on-the-fly model checking. In: Proc. 6th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol 818. Springer, Berlin Heidelberg New York, 1994, pp 377\u2013390","key":"93_CITPel94","DOI":"10.1007\/3-540-58179-0_69"},{"doi-asserted-by":"crossref","unstructured":"Stern U, Dill DL: Parallelizing the Murphy verifier. In: Proc. 9th International Conference on Computer Aided Verification, Lecture Notes in Computer Science, vol 1254. Springer, Berlin Heidelberg New York, 1997, pp 256\u2013267","key":"93_CITpmv","DOI":"10.1007\/3-540-63166-6_26"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0093-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10009-002-0093-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0093-2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-002-0093-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,12,15]],"date-time":"2024-12-15T16:38:11Z","timestamp":1734280691000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10009-002-0093-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2003,8]]},"references-count":21,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2003,8]]}},"alternative-id":["93"],"URL":"https:\/\/doi.org\/10.1007\/s10009-002-0093-2","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2003,8]]}}}