{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,17]],"date-time":"2025-09-17T15:56:17Z","timestamp":1758124577112},"reference-count":22,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2005,3,1]],"date-time":"2005-03-01T00:00:00Z","timestamp":1109635200000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Form Method Syst Des"],"published-print":{"date-parts":[[2005,3]]},"DOI":"10.1007\/s10703-005-1493-1","type":"journal-article","created":{"date-parts":[[2005,8,25]],"date-time":"2005-08-25T10:33:31Z","timestamp":1124966011000},"page":"197-219","source":"Crossref","is-referenced-by-count":6,"title":["Distributed Symbolic Model Checking for \u03bc-Calculus"],"prefix":"10.1007","volume":"26","author":[{"given":"Orna","family":"Grumberg","sequence":"first","affiliation":[]},{"given":"Tamir","family":"Heyman","sequence":"additional","affiliation":[]},{"given":"Assaf","family":"Schuster","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"1493_CR1","doi-asserted-by":"crossref","first-page":"496","DOI":"10.1007\/s10009-002-0093-2","volume":"4","author":"S. Ben-David","year":"2003","unstructured":"S. Ben-David, O. Grumberg, T. Heyman, and A. Schuster, \u201cScalable distributed on-the-fly symbolic model checking,\u201d Software Tools for Technology Transfer, Vol. 4 No. 4, pp. 496\u2013504, 2003.","journal-title":"Software Tools for Technology Transfer"},{"issue":"8","key":"1493_CR2","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\u2013691, 1986.","journal-title":"IEEE Transactions on Computers"},{"key":"1493_CR3","unstructured":"J.R. Burch, E.M. Clarke, and D.E. Long, \u201cSymbolic model checking with partitioned transition relations,\u201d in A. Halaas and P.B. Denyer (Eds.), Proceedings of the 1991 International Conference on Very Large Scale Integration, August 1991."},{"key":"1493_CR4","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, and L.J. Hwang, \u201cSymbolic model checking: 1020 states and beyond,\u201d Information and Computation, Vol. 98, No. 2, pp. 142\u2013171, 1992. Special Issue: Selections from 1990 IEEE Symposium on Logic in Computer Science.","DOI":"10.1016\/0890-5401(92)90017-A"},{"key":"1493_CR5","doi-asserted-by":"crossref","unstructured":"G. Cabodi, P. Camurati, and S. Quer, \u201cImproving the Efficient of BDD-bsaed operators by means of partitioning,\u201d IEEE Transactions on Computer-Aided Design, May 1999, pp. 545\u2013556.","DOI":"10.1109\/43.759068"},{"key":"1493_CR6","doi-asserted-by":"crossref","unstructured":"E.M. Clarke, E.A. Emerson, and A.P. Sistla, \u201cAutomatic verification of finite-state concurrent systems using temporal logic specifications,\u201d in Proceedings of the Tenth Annual ACM Symposium on Principles of Programming Languages, January 1983.","DOI":"10.1145\/567067.567080"},{"key":"1493_CR7","unstructured":"E.M. Clarke, O. Grumberg, and D.A. Peled, Model Checking, MIT press, December 1999."},{"key":"1493_CR8","doi-asserted-by":"crossref","first-page":"725","DOI":"10.1007\/BF00264284","volume":"27","author":"R. Cleaveland","year":"1990","unstructured":"R. Cleaveland, \u201cTableau-based model checking in the propositional \u03bc-calculus,\u201d Acta Informatica, Vol. 27, pp. 725\u2013747, 1990.","journal-title":"Acta Informatica"},{"key":"1493_CR9","first-page":"365","volume-title":"Workshop on Automatic Verification Methods for Finite State Systems","author":"O. Coudert","year":"1989","unstructured":"O. Coudert, J.C. Madre, and C. Berthet, \u201cVerifying of synchronous sequential machines based on symbolic execution,\u201d in J. Sifakis (Ed), Workshop on Automatic Verification Methods for Finite State Systems, Springer-Verlag: Grenoble, France, 1989, pp. 365\u2013373."},{"key":"1493_CR10","unstructured":"E.A. Emerson and C.-L. Lei, \u201cEfficient model checking in fragments of the propositional Mu-calculus,\u201d in Proceedings of the First Annual Symposium on Logic in Computer Science, IEEE Computer Society Press, June 1986."},{"key":"1493_CR11","unstructured":"Message Passing Interface Forum. MPI: A Message-Passing Interface standard. The International Journal of Supercomputer Applications and High Performance Computing, Vol. 8, 1994."},{"key":"1493_CR12","doi-asserted-by":"crossref","unstructured":"T. Heyman, D. Geist, O. Grumberg, and A. Schuster, \u201cAchieving scalability in parallel reachability analysis of very large circuits,\u201d in Proc. of the 12th International Conference on Computer Aided Verification, LNCS, 2000.","DOI":"10.1007\/10722167_6"},{"issue":"2","key":"1493_CR13","doi-asserted-by":"crossref","first-page":"317","DOI":"10.1023\/A:1020373206491","volume":"21","author":"T. Heyman","year":"2002","unstructured":"T. Heyman, D. Geist, O. Grumberg, and A. Schuster, \u201cAchieving scalability in parallel reachability analysis of very large circuits,\u201d Formal Methods in System Design, Vol. 21, No. 2, pp. 317\u2013338, 2002.","journal-title":"Formal Methods in System Design"},{"key":"1493_CR14","doi-asserted-by":"crossref","unstructured":"D. Kozen, Results on the propositional \u03bc-calculus, TCS, 27, 1983.","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"1493_CR15","doi-asserted-by":"crossref","unstructured":"O. Lichtenstein and A. Pnueli, \u201cChecking that finite state concurrent programs satisfy their linear specification,\u201d in Proceedings of the Twelfth Annual ACM Symposium on Principles of Programming Languages, January 1985, pp. 97\u2013107.","DOI":"10.1145\/318593.318622"},{"key":"1493_CR16","doi-asserted-by":"crossref","unstructured":"D. Long, A. Browne, E. Clark, S. jha, and W. Marrero, \u201cAn improved algorithm for the evaluation of fixpoint expressions,\u201d in Proc. of the Sixth International Conference on Computer Aided Verification, LNCS 818, 1994, pp. 338\u2013350.","DOI":"10.1007\/3-540-58179-0_66"},{"key":"1493_CR17","doi-asserted-by":"crossref","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, June 1997, pp. 388\u2013393.","DOI":"10.1109\/ICCAD.1997.643565"},{"key":"1493_CR18","doi-asserted-by":"crossref","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, June 1996, pp. 547\u2013554.","DOI":"10.1109\/ICCAD.1996.569909"},{"key":"1493_CR19","doi-asserted-by":"crossref","unstructured":"J.P. Quielle and J. Sifakis, \u201cSpecification and verification of concurrent systems in CESAR,\u201d in Proceedings of the Fifth International Symposium in Programming, 1981.","DOI":"10.1007\/3-540-11494-7_22"},{"key":"1493_CR20","doi-asserted-by":"crossref","unstructured":"C. Stirling and D.J. Walker, \u201cLocal model checking in the model mu-calculus,\u201d in Proc. of the 1989 Int. Joint Conf. on Theory and Practice of Software Development, 1989.","DOI":"10.1007\/3-540-50939-9_144"},{"key":"1493_CR21","doi-asserted-by":"crossref","first-page":"285","DOI":"10.2140\/pjm.1955.5.285","volume":"5","author":"A. Tarski","year":"1955","unstructured":"A. Tarski, \u201cA lattice-theoretical fixpoint theorem and its applications,\u201d Pacific J. Math, Vol. 5, pp. 285\u2013309, 1955.","journal-title":"Pacific J. Math"},{"key":"1493_CR22","doi-asserted-by":"crossref","unstructured":"G. Winskel, \u201cModel checking in the modal \u03bc-calculus,\u201d in Proceedings of the Sixteenth International Colloquium on Automata, Languages, and Programming, 1989.","DOI":"10.1007\/BFb0035797"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1493-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10703-005-1493-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10703-005-1493-1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,9]],"date-time":"2020-04-09T06:15:24Z","timestamp":1586412924000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10703-005-1493-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2005,3]]},"references-count":22,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2005,3]]}},"alternative-id":["1493"],"URL":"https:\/\/doi.org\/10.1007\/s10703-005-1493-1","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2005,3]]}}}