{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,2]],"date-time":"2026-10-02T07:15:08Z","timestamp":1790925308386,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540631668","type":"print"},{"value":"9783540691952","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1997]]},"DOI":"10.1007\/3-540-63166-6_26","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T18:13:46Z","timestamp":1330280026000},"page":"256-267","source":"Crossref","is-referenced-by-count":81,"title":["Parallelizing the Mur\u03d5 verifier"],"prefix":"10.1007","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","published-online":{"date-parts":[[2005,6,7]]},"reference":[{"key":"26_CR1","doi-asserted-by":"crossref","unstructured":"S. Aggarwal, R. Alonso, and C. Courcoubetis. Distributed reachability analysis for protocol verification environments. In Discrete Event Systems: Models and Applications. IIASA Conference, pages 40\u201356, 1987.","DOI":"10.1007\/BFb0042303"},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"A. Alexandrov, M. F. Ionescu, K. E. Schauser, and C. Scheiman. LogGP: incorporating long messages into the LogP model \u2014one step closer towards a realistic model for parallel computation. In 7th Annual ACM Symposium on Parallel Algorithms and Architectures, pages 95\u2013105, 1995.","DOI":"10.1145\/215399.215427"},{"key":"26_CR3","doi-asserted-by":"crossref","unstructured":"J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill. Sequential circuit verification using symbolic model checking. In 27th ACM\/IEEE Design Automation Conference, pages 46\u201351, 1990.","DOI":"10.1145\/123186.123223"},{"issue":"2","key":"26_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. Universal classes of hash functions. Journal of Computer and System Sciences, 18(2):143\u201354, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"26_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. LogP: towards a realistic model of parallel computation. In 4th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 1\u201312, 1993.","DOI":"10.1145\/155332.155333"},{"key":"26_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."},{"key":"26_CR7","doi-asserted-by":"crossref","unstructured":"D. L. Dill. The Mur\u03d5 verification system. In Computer Aided Verification. 8th International Conference, pages 390\u20133, 1996.","DOI":"10.1007\/3-540-61474-5_86"},{"key":"26_CR8","unstructured":"W. Feller. An Introduction to Probability Theory and Its Applications, volume 1. John Wiley & Sons, 3rd edition, 1968."},{"key":"26_CR9","unstructured":"G. J. Holzmann. On limits and possibilities of automated protocol analysis. In Protocol Specification, Testing, and Verification. 7th International Conference, pages 339\u201344, 1987."},{"key":"26_CR10","doi-asserted-by":"crossref","unstructured":"G. J. Holzmann and D. Peled. The state of SPIN. In Computer Aided Verification. 8th International Conference, pages 385\u20139, 1996.","DOI":"10.1007\/3-540-61474-5_85"},{"key":"26_CR11","doi-asserted-by":"crossref","unstructured":"A. J. Hu, G. York, and D. L. Dill. New techniques for efficient verification with implicitly conjoined BDDs. In 31st Design Automation Conference, pages 276\u201382, 1994.","DOI":"10.1145\/196244.196377"},{"key":"26_CR12","unstructured":"IEEE Std 1596\u20131992, IEEE Standard for Scalable Coherent Interface (SCI)."},{"key":"26_CR13","unstructured":"C. N. Ip. State Reduction Methods for Automatic Formal Verification. PhD thesis, Stanford University, 1996."},{"key":"26_CR14","doi-asserted-by":"crossref","unstructured":"S. Kimura and E. M. Clarke. A parallel algorithm for constructing binary decision diagrams. In IEEE International Conference on Computer Design, pages 220\u20133, 1990.","DOI":"10.1109\/ICCD.1990.130209"},{"key":"26_CR15","doi-asserted-by":"crossref","unstructured":"N. Kumar and R. Vemuri. Finite state machine verification on MIMD machines. In European Design Automation Conference, pages 514\u201320, 1992.","DOI":"10.1109\/EURDAC.1992.246312"},{"key":"26_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. The Stanford FLASH multiprocessor. In 21st Annual International Symposium on Computer Architecture, pages 302\u201313, 1994.","DOI":"10.1109\/ISCA.1994.288140"},{"issue":"3","key":"26_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. The Stanford DASH multiprocessor. Computer, 25(3):63\u201379, 1992.","journal-title":"Computer"},{"key":"26_CR18","doi-asserted-by":"crossref","unstructured":"R. P. Martin, A. M. Vahdat, D. E. Culler, and T. E. Anderson. Effects of communication latency, overhead, and bandwidth in a cluster architecture. In 24th Annual International Symposium on Computer Architecture, 1997.","DOI":"10.1145\/264107.264146"},{"key":"26_CR19","doi-asserted-by":"crossref","unstructured":"R. K. Ranjan, J. V. Sanghavi, R. K. Brayton, and A. Sangiovanni-Vincentelli. Binary decision diagrams on network of workstations. In International Conference on Computer Design, pages 358\u201364, 1996.","DOI":"10.1109\/ICCD.1996.563579"},{"key":"26_CR20","doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. Improved probabilistic verification by hash compaction. In Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pages 206\u201324, 1995.","DOI":"10.1007\/3-540-60385-9_13"},{"key":"26_CR21","doi-asserted-by":"crossref","unstructured":"U. Stern and D. L. Dill. A new scheme for memory-efficient probabilistic verification. In Joint International Conference on Formal Description Techniques for Distributed Systems and Communication Protocols, and Protocol Specification, Testing, and Verification, pages 333\u201348, 1996.","DOI":"10.1007\/978-0-387-35079-0_21"},{"key":"26_CR22","doi-asserted-by":"crossref","unstructured":"T. Stornetta. Implementation of an efficient parallel BDD package. Master's thesis, UC Santa Barbara, 1995.","DOI":"10.1145\/240518.240639"},{"key":"26_CR23","doi-asserted-by":"crossref","unstructured":"T. Stornetta and F. Brewer. Implementation of an efficient parallel BDD package. In 33rd Design Automation Conference, pages 641\u20134, 1996.","DOI":"10.1145\/240518.240639"},{"key":"26_CR24","doi-asserted-by":"crossref","unstructured":"T. von Eicken, D. E. Culler, S. C. Goldstein, and K. E. Schauser. Active messages: a mechanism for integrated communication and computation. In 19th Annual International Symposium on Computer Architecture, pages 256\u201366, 1992.","DOI":"10.1145\/139669.140382"},{"key":"26_CR25","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":"26_CR26","doi-asserted-by":"crossref","unstructured":"P. Wolper and D. Leroy. Reliable hashing without collision detection. In Computer Aided Verification. 5th International Conference, pages 59\u201370, 1993.","DOI":"10.1007\/3-540-56922-7_6"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-63166-6_26.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T16:16:42Z","timestamp":1605629802000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-63166-6_26"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1997]]},"ISBN":["9783540631668","9783540691952"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/3-540-63166-6_26","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1997]]}}}