The CMurphi verifier is the result of our research on Explicit State Space Exploration.

CMurphi is based on the Murphi verifier from Stanford University. The original Murphi version 3.1 has been extensively bug-fixed and extended to support our new cache and disk-based verification algorithms, namely CBFS and LDBFS. Moreover, from version 4.2, the CMurphi verifier extends the Murphi input language with finite precision real numbers.

CMurphi verifiers can be compiled in three modes:

  • Murphi 3.1 Mode: the verifier works like the original Murphi 3.1, using main memory for the visited states hash table and the verification queue.
  • Cache Mode: the verifier uses a cache to store the visited states and can extend the verification queue to disk. By exploiting the transition locality of certain software, in particular protocols, this kind of verifier can explore protocols much larger than the available memory. The cache collision rate can be monitored to stop the exploration if the cache becomes ineffective.
  • Disk Mode: the verifier uses the disk to store the visited states and the verification queue. In this modality the verifier can explore models of any size and the termination is always ensured. The disk access rate is adjusted dynamically by the algorithm to read the smallest set of states needed to terminate the exploration, thus drastically reducing the time overhead due to disk accesses.

What's New (updated: June 19, 2012 )

  • CMurphi and its extensions are now maintained by Igor Melatti at the Sapienza Model Checking Group. Please refer to the corresponding web page for the latest releases of the tool.
  • A maintainance release (4.25) has been released on May 5, 2004.
    The 'write violating trace' option (-tv) is now available also in disk-Murphi mode, thanks to Igor Melatti. The support for this option has also been improved for the cached-Murphi mode. Some other minor problems have been fixed.
  • A new CMurphi version (4.2) has been released on October 1,2003.
    In the new version, the Murphi input language (in Standard, Disk and Cache mode) supports the new data type REAL(scale,precision) (finite precision real number), floating point constants (in decimal or exponential format) and accepts all the floating point functions defined in the standard C header file math.h. 

Getting and Installing CMurphi

CMurphi can be compiled on a large number of different platforms, including Linux and Windows (under the cygwin environment).

The CMurphi package contains the complete source files, documentation and example protocols from the original Murphi 3.1 distribution. The CMurphi verifier is provided "as is" and without warranties of any kind.

  • To download the latest CMurphi release, go to the CMurphi web page @ La Sapienza.
  • The latest CMurphi package developed by the L'Aquila Model Checking Group (version 4.25) is available here (1,6Mb tgz file). Note that this release could not compile on newer Linux distributions.
  • You can also download the previous version (4.1) from here.

To install CMurphi, simply unpack the downloaded archive, then go to the src/ subdirectory and type make. This will build the CMurphi compiler (mu).

The CMurphi compiler can be used to compile verifiers from the source files  (files with .m extension - many examples are in the ex/ subdirectory). You can use the --cache and --disk switches to compile verifiers in cache or disk mode, respectively. For further instructions read the README.cmurphi contained in the CMurphi root directory.

Exploring the CMurphi Code

CMurphi is released under the same license of Murphi 3.1. You can freely modify the sources, but you cannot redistribute modified sources without the explicit authors' permission.

The include/ distribution directory contains the source code used to build the CMurphi verifiers. The disk and cache algorithms are contained in two separate subdirectories, namely murphi.disk/ and muprhi.cache/. Before attempting to read or modify the sources, please read the README.cmurphi files in the corresponding directory.

CMurphi Examples

You can look at some results obtained using the cache and disk algorithms on the murphi experiments page.