{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T09:39:01Z","timestamp":1791106741766,"version":"4.1.0"},"reference-count":28,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2001,3,1]],"date-time":"2001-03-01T00:00:00Z","timestamp":983404800000},"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":[[2001,3]]},"DOI":"10.1023\/a:1008771324652","type":"journal-article","created":{"date-parts":[[2002,12,22]],"date-time":"2002-12-22T11:37:32Z","timestamp":1040557052000},"page":"117-129","source":"Crossref","is-referenced-by-count":34,"title":["Parallelizing the Mur\u03d5 Verifier"],"prefix":"10.1007","volume":"18","author":[{"given":"Ulrich","family":"Stern","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"David L.","family":"Dill","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"315468_CR1","doi-asserted-by":"crossref","unstructured":"S. Aggarwal, R. Alonso, and C. Courcoubetis, \u201cDistributed reachability analysis for protocol verification environments,\u201d in Discrete Event Systems: Models and Applications, IIASA Conference, 1987, pp. 40\u201356.","DOI":"10.1007\/BFb0042303"},{"key":"315468_CR2","doi-asserted-by":"crossref","unstructured":"A. Alexandrov, M.F. Ionescu, K.E. Schauser, and C. Scheiman, \u201cLogGP: Incorporating long messages into the LogP model\u2014one step closer towards a realistic model for parallel computation,\u201d in 7th Annual ACM Symposium on Parallel Algorithms and Architectures, 1995, pp. 95\u2013105.","DOI":"10.1145\/215399.215427"},{"key":"315468_CR3","doi-asserted-by":"crossref","unstructured":"J.R. Burch, E.M. Clarke, K.L. McMillan, and D.L. Dill, \u201cSequential circuit verification using symbolic model checking,\u201d in 27th ACM\/IEEE Design Automation Conference, 1990, pp. 46\u201351.","DOI":"10.1145\/123186.123223"},{"issue":"2","key":"315468_CR4","doi-asserted-by":"crossref","first-page":"143","DOI":"10.1016\/0022-0000(79)90044-8","volume":"18","author":"J.L. Carter","year":"1979","unstructured":"J.L. Carter and M.N. Wegman, \u201cUniversal classes of hash functions,\u201d Journal of Computer and System Sciences,\u201d Vol. 18, No. 2, 143\u2013154, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"315468_CR5","doi-asserted-by":"crossref","unstructured":"D. Culler, R. Karp, D. Patterson, A. Sahay, K.E. Schauser, E. Santos, R. Subramonian, and T. von Eicken, \u201cLogP: Towards a realistic model of parallel computation,\u201d in 4th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 1993, pp. 1\u201312.","DOI":"10.1145\/155332.155333"},{"key":"315468_CR6","unstructured":"D. Culler, K. Keeton, C. Krumbein, L.T. Liu, A. Mainwaring, R. Martin, S. Rodrigues, K. Wright, and C. Yoshikawa, Generic Active Message Interface Specification, UC Berkeley, 1995. Version 1.1 http:\/\/ now.cs.berkeley.edu\/papers2\/."},{"key":"315468_CR7","doi-asserted-by":"crossref","unstructured":"D.L. Dill, \u201cThe Mur' verification system,\u201d in Computer Aided Verification, 8th International Conference, 1996, pp. 390\u2013393.","DOI":"10.1007\/3-540-61474-5_86"},{"key":"315468_CR8","volume-title":"An Introduction to Probability Theory and Its Applications","author":"W. Feller","year":"1968","unstructured":"W. Feller, An Introduction to Probability Theory and Its Applications, vol. 1, John Wiley & Sons, New York, 3rd ed. 1968.","edition":"3rd ed."},{"key":"315468_CR9","unstructured":"G.J. Holzmann, \u201cOn limits and possibilities of automated protocol analysis,\u201d in Protocol Specification, Testing, and Verification, 7th International Conference, 1987. pp. 339\u2013344."},{"key":"315468_CR10","doi-asserted-by":"crossref","unstructured":"G.J. Holzmann and D. Peled, \u201cThe state of SPIN,\u201d in Computer Aided Verification, 8th International Conference, 1996, pp. 385\u2013389.","DOI":"10.1007\/3-540-61474-5_85"},{"key":"315468_CR11","unstructured":"A.J. Hu, \u201cTechniques for efficient formal verification using binary decision diagrams,\u201d PhD thesis, Stanford University, 1995."},{"key":"315468_CR12","unstructured":"IEEE Std 1596-1992, IEEE Standard for Scalable Coherent Interface (SCI)."},{"key":"315468_CR13","unstructured":"C.N. Ip, \u201cState reduction methods for automatic formal verification,\u201d PhD thesis, Stanford University, 1996."},{"key":"315468_CR14","doi-asserted-by":"crossref","unstructured":"S. Kimura and E.M. Clarke, \u201cA parallel algorithm for constructing binary decision diagrams,\u201d in IEEE International Conference on Computer Design, 1990, pp. 220\u2013223.","DOI":"10.1109\/ICCD.1990.130209"},{"key":"315468_CR15","doi-asserted-by":"crossref","unstructured":"N. Kumar and R. Vemuri, \u201cFinite state machine verification on MIMD machines,\u201d in European Design Automation Conference, 1992, pp. 514\u2013520.","DOI":"10.1109\/EURDAC.1992.246312"},{"key":"315468_CR16","doi-asserted-by":"crossref","unstructured":"J. Kuskin, D. Ofelt, M. Heinrich, J. Heinlein, R. Simoni, K. Gharachorloo, J. Chapin, D. Nakahira, J. Baxter, M. Horowitz, A. Gupta, M. Rosenblum, and J. Hennessy, \u201cThe Stanford FLASH multiprocessor,\u201d in 21st Annual International Symposium on Computer Architecture, 1994, pp. 302\u2013313.","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"3","key":"315468_CR17","doi-asserted-by":"crossref","first-page":"63","DOI":"10.1109\/2.121510","volume":"25","author":"D. Lenoski","year":"1992","unstructured":"D. Lenoski, J. Laudon, K. Gharachorloo, W.-D. Weber, A. Gupta, J. Hennessy, M. Horowitz, and M.S. Lam, \u201cThe Stanford DASH multiprocessor. Computer,\u201d Vol. 25 No. 3, pp. 63\u201379, 1992.","journal-title":"Computer"},{"key":"315468_CR18","doi-asserted-by":"crossref","unstructured":"R.P. Martin, A.M. Vahdat, D.E. Culler, and T.E. Anderson, \u201cEffects of communication latency, overhead, and band width in a cluster architecture,\u201d in 24th Annual International Symposium on Computer Architecture, 1997.","DOI":"10.1145\/264107.264146"},{"key":"315468_CR19","doi-asserted-by":"crossref","unstructured":"R.K. Ranjan, J.V. Sanghavi, R.K. Brayton, and A. Sangiovanni-Vincentelli, \u201cBinary decision diagrams on network of workstations,\u201d in International Conference on Computer Design, 1996, pp. 358\u2013364.","DOI":"10.1109\/ICCD.1996.563579"},{"key":"315468_CR20","unstructured":"U. Stern, \u201cAlgorithmic techniques in verification by explicit state enumeration,\u201d PhD thesis, Technical University of Munich, 1997."},{"key":"315468_CR21","doi-asserted-by":"crossref","unstructured":"U. Stern and D.L. Dill, Using magnetic disk instead of main memory in the Mur\u03d5 verifier, Computer Aided Verification, 10th International Conference, 1998, pp. 172\u2013183.","DOI":"10.1007\/BFb0028743"},{"key":"315468_CR22","doi-asserted-by":"crossref","unstructured":"U. Stern and D.L. Dill, \u201cA new scheme for memory-efficient probabilistic verification,\u201d in Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, 1996, pp. 333\u2013348.","DOI":"10.1007\/978-0-387-35079-0_21"},{"key":"315468_CR23","doi-asserted-by":"crossref","unstructured":"U. Stern and D.L. Dill, \u201cParallelizing the Mur\u03d5 verifier,\u201d in Computer Aided Verification, 9th International Conference, 1997, pp. 256\u2013267.","DOI":"10.1007\/3-540-63166-6_26"},{"key":"315468_CR24","unstructured":"T. Stornetta, \u201cImplementation of an efficient parallel BDD package,\u201d Master's thesis, UC Santa Barbara, 1995."},{"key":"315468_CR25","doi-asserted-by":"crossref","unstructured":"T. Stornetta and F. Brewer, \u201cImplementation of an efficient parallel BDD package,\u201d in 33rd Design Automation Conference, 1996, pp. 641\u2013644.","DOI":"10.1109\/DAC.1996.545653"},{"key":"315468_CR26","doi-asserted-by":"crossref","unstructured":"T. von Eicken, D.E. Culler, S.C. Goldstein, and K.E. Schauser, \u201cActive messages: A mechanism for integrated communication and computation,\u201d in 19th Annual International Symposium on Computer Architecture, 1992, pp. 256\u2013266.","DOI":"10.1109\/ISCA.1992.753322"},{"key":"315468_CR27","unstructured":"C.-P. Wen, A distributed task queue for load balancing on the CM5. Unpublished paper written in Katherine Yelick's group at UC Berkeley."},{"key":"315468_CR28","doi-asserted-by":"crossref","unstructured":"P. Wolper and D. Leroy, \u201cReliable hashing without collision detection,\u201d in Computer Aided Verification. 5th International Conference, 1993, pp. 59\u201370.","DOI":"10.1007\/3-540-56922-7_6"}],"container-title":["Formal Methods in System Design"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008771324652.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1023\/A:1008771324652\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1023\/A:1008771324652.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,8,5]],"date-time":"2025-08-05T19:09:48Z","timestamp":1754420988000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1023\/A:1008771324652"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2001,3]]},"references-count":28,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2001,3]]}},"alternative-id":["315468"],"URL":"https:\/\/doi.org\/10.1023\/a:1008771324652","relation":{},"ISSN":["0925-9856","1572-8102"],"issn-type":[{"value":"0925-9856","type":"print"},{"value":"1572-8102","type":"electronic"}],"subject":[],"published":{"date-parts":[[2001,3]]}}}