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.
You can look at some results obtained using the cache and disk algorithms on
the murphi experiments page.