Abstract
Murϕ is a formal verification system for finite-state concurrent systems developed as a research project at Stanford University. It has been widely used for many protocols especially for multiprocessor cache coherence protocols and cryptographic protocols. This paper reviews the history of Murϕ, some of results that of the project, and lessons learned.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Mitchell, J.C., Mitchell, M., Stern, U.: Automated analysis of cryptographic protocols using murφ. In: IEEE Symposium on Security and Privacy, pp. 141–153 (1997)
Mitchell, J.C.: Finite-state analysis of security protocols. In: Computer Aided Verification. LNCS, pp. 71–76 (1998)
Lenoski, D., Laudon, J., Gharachorloo, K., Weber, W.D., Gupta, A., Hennessy, J., Horowitz, M., Lam, M.: The Stanford DASH multiprocessor. Computer 25(3) (1992)
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)
Bryant, R.E.: Graph-based algorithms for Boolean function manipulation. IEEE Transactions on Computers C-35(8) (1986)
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–251 (1991)
Chandy, K.M., Misra, J.: Parallel Program Design — a Foundation. Addison-Wesley (1988)
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)
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–525 (1992)
Hu, A.J., Dill, D.L.: Reducing BDD size by exploiting functional dependencies. In: 30th Design Automation Conference, pp. 266–271 (1993)
Hu, A.J., Dill, D.L.: Efficient verification with BDDs using implicitly conjoined invariants. In: 5th International Conference on Computer-Aided Verification (1993)
Hu, A.J., York, G., Dill, D.L.: New techniques for efficient verification with implicitly conjoined bdds. In: 31th Design Automation Conference, pp. 276–282 (1994)
Ip, C.N., Dill, D.L.: Better verification through symmetry. In: 11th International Symposium on Computer Hardware Description Languages and Their Applications, pp. 87–100 (1993)
Ip, C.N., Dill, D.L.: Better verification through symmetry. Formal Methods in System Design 9(1/2), 41–75 (1996)
Clarke, E., Enders, R., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. Formal Methods in System Design 9(1/2), 77–104 (1996)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design 9(1/2), 105–131 (1996)
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)
Gyuris, V., Sistla, A.P.: On-the-fly model checking under fairness that exploits symmetry. Formal Methods in System Design 15(3), 217–238 (1999)
Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Protocol Specification, Testing, and Verification. 7th International Conference, pp. 339–344 (1987)
Holzmann, G.J.: Design and Validation of Computer Protocols. Prentice-Hall, Englewood Cliffs (1991)
Wolper, P., Leroy, D.: Reliable hashing without collision detection. In: Computer Aided Verification. 5th International Conference, pp. 59–70 (1993)
Wolper, P., Leroy, D.: Reliable hashing without collision detection (unpublished revised version of [21])
Roscoe, A.: Model-checking CSP. Prentice-Hall (1994)
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 9(2), 133–166 (2000)
Holzmann, G.: Design and validation of computer protocols. Prentice-Hall (1991)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Dill, D.L. (2008). A Retrospective on Murϕ . In: Grumberg, O., Veith, H. (eds) 25 Years of Model Checking. Lecture Notes in Computer Science, vol 5000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69850-0_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-69850-0_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69849-4
Online ISBN: 978-3-540-69850-0
eBook Packages: Computer ScienceComputer Science (R0)