RAISE CMurphi (Caching Murphi)
CMurphi (Caching Murphi) is a model checker developed on the top of Murphi.
CMurphi (Caching Murphi) is a model checker developed on the top of Murphi. The original Murphi web page is here (via the Wayback machine).
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.
These algorithms are described in the following publication:
Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems, 2004
@article{dellapenna-etal:2004:sttt,
author = {Della Penna, G. and Intrigila, B. and Melatti, I. and Tronci, E. and Venturini Zilli, M.},
title = {Exploiting Transition Locality in Automatic Verification of Finite State Concurrent Systems},
doi = {10.1007/s10009-004-0149-6},
journal = {International Journal on Software Tools for Technology Transfer},
number = {4},
pages = {320--341},
publisher = {Springer},
volume = {6},
year = {2004}
}