Murφ

Murφ's early history is described in a paper by David Dill.{{cite book |last1=Dill |first1=David L. |author1-link=A Retrospective on Murϕ |editor1-last=Grumberg |editor1-first=Orna |editor2-last=Veith |editor2-first=Helmut |title=25 Years of Model Checking: History, Achievements, Perspectives |date=2008 |pages=77–88}} The first version of Murφ was designed at Stanford University in 1990 and 1991 by Prof. David Dill and his graduate students Andreas Drexler, Alan Hu, and Han Yang, and primarily implemented by Andreas Drexler. The specification language was extensively modified and extended by David Dill, Alan Hu, C. Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang. Ralph Melton implemented the new version during the summer and fall of 1992. Seungjoon Park added liveness checking and fairness constraints, but because the algorithm for liveness verification conflicted with important optimizations, particularly symmetry reduction, liveness verification was omitted in subsequent releases. C. Norris Ip implemented reversible rules and repetition constructors (which are not included in release 3.1), and added symmetry and multiset reductions (which are). Ulrich Stern implemented hash compaction,{{cite book |last1=Stern |first1=Ulrich |last2=Dill |first2=David L. |title=Formal Description Techniques IX |date=1996 |publisher=Springer |location=Boston, MA |pages=333–348}} improved the use of disk, and implemented Parallel Murφ.

The last release from Stanford was release 3.1 in November of 1993. Many derivative versions of Murφ have been created since then by other groups.

The Murφ compiler accepts a model written in the Murφ specification language and outputs C++ code that constitutes a verifier for that model. (That is, the C++ code, when executed, performs explicit-state model checking on the design described by the specification.) The

[https://github.com/melver/cmurphi/blob/master/doc/User.Manual Murφ specification language] uses guarded commands and an asynchronous, interleaving model of concurrency, with all synchronization and communication done through global variables.

The verifier checks safety properties in the form of invariants and internal assertions that are specified in the model, and checks for deadlock. It does not check liveness

properties, though Murφ release 2.7L did support verification of a set of common LTL liveness properties. The language and verifier support some kinds of symmetry reductions.{{cite book |last1=Ip |first1=C. Norris |last2=Dill |first2=David L. |title=Proceedings of 1993 IEEE International Conference on Computer Design ICCD'93 |chapter=Efficient verification of symmetric concurrent systems |date=1993 |pages=230–234 |publisher=IEEE|doi=10.1109/ICCD.1993.393375 |isbn=0-8186-4230-0 |s2cid=38444364 }}

Murφ was originally applied to verifying cache-coherence protocols,{{cite journal |last1=Dill |first1=David L. |last2=Drexler |first2=Andreas J. |last3=Hu |first3=Alan J. |last4=Yang |first4=C. Han |title=Protocol verification as a hardware design aid |journal=Proceedings of the 1992 IEEE International Conference on Computer Design: VLSI in Computers & Processors |date=1992 |pages=552–525 |publisher=IEEE}} but has been applied to other problems as well, including [http://seclab.stanford.edu/pcl/mc/mc.html verification of security protocols].

The Murφ license is similar to the MIT license. Murφ may be used, copied, modified, sold, and redistributed for any purpose, provided the copyright notice and license are included, the name of Stanford University is not used for advertising or publicity without permission, and modified versions are not called Murphi without permission.

Many derivative versions of Murφ have been created, at Stanford and elsewhere, including these:

• Parallel Murφ
• [http://formalverification.cs.utah.edu/EddyMurphi/ Eddy — Parallel and distributed Murφ.]
• [https://www.cs.ubc.ca/~depaulfm/PReach.html PReach (Parallel Reachability) — Parallel model checking implemented in Erlang.]
• [http://formalverification.cs.utah.edu/Murphi/ Distributed Murphi]
• [http://formalverification.cs.utah.edu/Murphi/ Parallel Random-Walk Murphi]
• [http://formalverification.cs.utah.edu/Murphi/ PAM — Predicate Abstraction Murphi]
• [http://formalverification.cs.utah.edu/Murphi/ POeM — Partial-Order Enabled Murphi]
• [http://mclab.di.uniroma1.it/site/index.php/software/18-cmurphi CMurphi — Caching Murphi.]
• [http://mclab.di.uniroma1.it/site/index.php/software/17-fhp-murphi FHP-Murphi — Finite Horizon Probabilistic Murphi.]
• [http://formalverification.cs.utah.edu/EddyMurphi/ Eddy Murphi — Parallel and distributed, based on CMurphi, using MPI for message passing.]
• [https://github.com/gdellapenna/UPMurphi Universal Planner Murphi — Planning and universal planning for linear and nonlinear continuous PDDL+ models with processes and events; also timed initial literals and timed initial fluents.]
• [https://github.com/Smattr/rumur rumur]

• Model checking
• list of model checking tools

{{Reflist}}

• [https://github.com/melver/cmurphi/blob/master/doc/User.Manual Murphi Annotated Reference Manual, Release 3.1]
• [http://seclab.stanford.edu/pcl/mc/mc.html Stanford Security Lab, Model Checking Methods for Security Protocols]
• [http://formalverification.cs.utah.edu/Murphi/ University of Utah, School of Computing — a collection of versions of Murφ.]

Category:Model checking

Category:Free software programmed in C++