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.
The specification language was extensively modified and extended by David Dill, Alan Hu, C. Norris Ip, Ralph Melton, Seungjoon Park, and Han Yang.
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).
The Murφ specification language uses guarded commands and an asynchronous, interleaving model of concurrency, with all synchronization and communication done through global variables.
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.