Model Checking Laboratory

CMurphi

Details

Category: Software

Last Updated on Friday, 23 July 2021 21:54

CMurphi (Caching Murphi) is a model checker developed on the top of Murphi.

The bitbucket page for Cmurphi is here (not actively maintained)

The original Murphi web page is here, while a more up-to-date page is here.

CMurphi implements two new model checking algorithms. The first one has been obtained from Murphi 3.1 release by replacing Murphi Hash Table with a Cache and Murphi RAM queue with a disk queue. The second one is disk based. Both are described in [STTT 2004].

The current version of CMurphi is a refactored one:

• it corrects some errors coming out with newer versions of g++
• it supports 64-bit architectures also when using hash compaction
• it includes FHP-Murphi

The current version of CMurphi (as of 2021/07/23) may be downloaded here (CMurphi 5.5.0).

The original Murphi web page is here (Stanford University), while a more up-to-date page is here (University of Utah).

All versions of CMurphi are listed below.