Murφ (/ˈmɝ.fi/, also spelled Murphi) is an explicit-state model checker developed at Stanford University, and widely used for formal verification of cache-coherence protocols.

History

Murφ's early history is described in a paper by David Dill. 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, 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.

Features

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.) Th
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. Murφ was originally applied to verifying cache-coherence protocols, but has been applied to other problems as well, includin
verification of security protocols

Licensing

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.

Derivatives

Many derivative versions of Murφ have been created, at Stanford and elsewhere, including these: * Parallel Murφ
Eddy — Parallel and distributed Murφ.

* ttp://formalverification.cs.utah.edu/Murphi/ Distributed Murphi
Parallel Random-Walk Murphi

PAM — Predicate Abstraction Murphi

POeM — Partial-Order Enabled Murphi

CMurphi — Caching Murphi.

FHP-Murphi — Finite Horizon Probabilistic Murphi.

Eddy Murphi — Parallel and distributed, based on CMurphi, using MPI for message passing.

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.

rumur

References

{{Reflist

External links