{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,3]],"date-time":"2026-10-03T20:20:32Z","timestamp":1791058832145,"version":"4.1.0"},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540698494","type":"print"},{"value":"9783540698500","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-69850-0_5","type":"book-chapter","created":{"date-parts":[[2008,7,31]],"date-time":"2008-07-31T02:39:46Z","timestamp":1217471986000},"page":"77-88","source":"Crossref","is-referenced-by-count":2,"title":["A Retrospective on Mur\u03d5"],"prefix":"10.1007","author":[{"given":"David L.","family":"Dill","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using mur\u03c6. In: IEEE Symposium on Security and Privacy, pp. 141\u2013153 (1997)","DOI":"10.1109\/SECPRI.1997.601329"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Mitchell, J.C.: Finite-state analysis of security protocols. In: Computer Aided Verification. LNCS, pp. 71\u201376 (1998)","DOI":"10.1007\/BFb0028734"},{"key":"5_CR3","doi-asserted-by":"crossref","unstructured":"Lenoski, D., Laudon, J., Gharachorloo, K., Weber, W.D., Gupta, A., Hennessy, J., Horowitz, M., Lam, M.: The Stanford DASH multiprocessor. Computer\u00a025(3) (1992)","DOI":"10.1109\/2.121510"},{"key":"5_CR4","unstructured":"Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, L.: Symbolic model checking: 1020 states and beyond. In: 5th IEEE Symposium on Logic in Computer Science (1990)"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers\u00a0C-35(8) (1986)","DOI":"10.1109\/TC.1986.1676819"},{"key":"5_CR6","unstructured":"McMillan, K.L., Schwalbe, J.: Formal verification of the gigamax cache-consistency protocol. In: Proceedings of the International Symposium on Shared Memory Multiprocessing, Information Processing Society of Japan, pp. 242\u2013251 (1991)"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"Chandy, K.M., Misra, J.: Parallel Program Design \u2014 a Foundation. Addison-Wesley (1988)","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"5_CR8","doi-asserted-by":"crossref","unstructured":"Nowatzyk, A., Aybay, G., Browne, M., Kelly, E., Parkin, M., Radke, W., Vishin, S.: The s3.mp scalable shared memory multiprocessor. In: International Conference on Parallel Processing (1995)","DOI":"10.1109\/HICSS.1994.323149"},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"Dill, D.L., Drexler, A.J., Hu, A.J., Yang, C.H.: Protocol verification as a hardware design aid. In: IEEE International Conference on Computer Design: VLSI in Computers and Processors, pp. 522\u2013525 (1992)","DOI":"10.1109\/ICCD.1992.276232"},{"key":"5_CR10","doi-asserted-by":"crossref","unstructured":"Hu, A.J., Dill, D.L.: Reducing BDD size by exploiting functional dependencies. In: 30th Design Automation Conference, pp. 266\u2013271 (1993)","DOI":"10.1145\/157485.164888"},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"Hu, A.J., Dill, D.L.: Efficient verification with BDDs using implicitly conjoined invariants. In: 5th International Conference on Computer-Aided Verification (1993)","DOI":"10.1007\/3-540-56922-7_2"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"Hu, A.J., York, G., Dill, D.L.: New techniques for efficient verification with implicitly conjoined bdds. In: 31th Design Automation Conference, pp. 276\u2013282 (1994)","DOI":"10.1145\/196244.196377"},{"key":"5_CR13","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. In: 11th International Symposium on Computer Hardware Description Languages and Their Applications, pp. 87\u2013100 (1993)"},{"issue":"1\/2","key":"5_CR14","first-page":"41","volume":"9","author":"C.N. Ip","year":"1996","unstructured":"Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design\u00a09(1\/2), 41\u201375 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"1\/2","key":"5_CR15","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF00625969","volume":"9","author":"E. Clarke","year":"1996","unstructured":"Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design\u00a09(1\/2), 77\u2013104 (1996)","journal-title":"Formal Methods in System Design"},{"issue":"1\/2","key":"5_CR16","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/BF00625970","volume":"9","author":"E.A. Emerson","year":"1996","unstructured":"Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design\u00a09(1\/2), 105\u2013131 (1996)","journal-title":"Formal Methods in System Design"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"Emerson, E., Sistla, A.: Utilizing symmetry when model checking under fairness assumptions: An automata-theoretic approach. In: 7th International Conference on Computer-Aided Verification (1995)","DOI":"10.1007\/3-540-60045-0_59"},{"issue":"3","key":"5_CR18","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1023\/A:1008701202999","volume":"15","author":"V. Gyuris","year":"1999","unstructured":"Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. Formal Methods in System Design\u00a015(3), 217\u2013238 (1999)","journal-title":"Formal Methods in System Design"},{"key":"5_CR19","unstructured":"Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Protocol Specification, Testing, and Verification. 7th International Conference, pp. 339\u2013344 (1987)"},{"key":"5_CR20","volume-title":"Design and Validation of Computer Protocols","author":"G.J. Holzmann","year":"1991","unstructured":"Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)"},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Computer Aided Verification. 5th International Conference, pp. 59\u201370 (1993)","DOI":"10.1007\/3-540-56922-7_6"},{"key":"5_CR22","unstructured":"Wolper, P., Leroy, D.: Reliable hashing without collision detection (unpublished revised version of [21])"},{"key":"5_CR23","unstructured":"Roscoe, A.: Model-checking CSP. Prentice-Hall (1994)"},{"issue":"2","key":"5_CR24","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/350887.350891","volume":"9","author":"A.P. Sistla","year":"2000","unstructured":"Sistla, A.P., Gyuris, V., Emerson, E.A.: Smc: a symmetry-based model checker for verification of safety and liveness properties. ACM Transactions Software Engineering Methodolgy\u00a09(2), 133\u2013166 (2000)","journal-title":"ACM Transactions Software Engineering Methodolgy"},{"key":"5_CR25","unstructured":"Holzmann, G.: Design and validation of computer protocols. Prentice-Hall (1991)"}],"container-title":["Lecture Notes in Computer Science","25 Years of Model Checking"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-69850-0_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,3]],"date-time":"2021-05-03T00:10:14Z","timestamp":1620000614000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-69850-0_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540698494","9783540698500"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-69850-0_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}