Caching Murphi

Caching Murphi 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 original Murphi 3.1 release can be obtained from http://sprout.stanford.edu/dill/murphi.html .

Caching Murphi 3.1

Here is the paper describing the caching approach of Caching Murphi (Release 3.1)

[TDIZ 01]
Enrico Tronci, Giuseppe Della Penna, Benedetto Intrigila, Marisa Venturini Zilli,
Exploiting Transition Locality in Automatic Verification ,
Proceedings of: 11th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), 4-7 September 2001, Livingston-Edinburgh (Scotland), LNCS, Springer-Verlag
Co-sponsored by the IFIP TC10/WG10.5 Working Group on: Design and Engineering of Electronic Systems
Abstract

Caching Murphi 4.1

Caching Murphi 4.1 adds to caching murphi 3.1 the disk based verification algorithm described in the following paper.

[DITZ 02]
Giuseppe Della Penna, Benedetto Intrigila, Enrico Tronci, Marisa Venturini Zilli,
Exploiting Transition Locality in the Disk Based Murphi Verifier,
Proceedings of 4th International Conference on: Formal Methods in Computer Aided Verification (FMCAD 2002), Nov. 2002, Portland, Oregon, USA, LNCS, Springer
Abstract

Caching Murphi 4.2

Caching Murphi 4.2 adds to caching murphi 4.1 finite precision real numbers as described in the following paper.

[DIMMCPTZ03]
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Michele Minichino, Ester Ciancamerla, Andrea Parisse, Enrico Tronci, Marisa Venturini Zilli,
Automatic Verification of a Turbogas Control System with the Murphi Verifier,
Proceedings of: 6th International Workshop Hybrid Systems: Computation and Control (HSCC) April 2003, Prague, Czech Republic, LNCS 2623, Springer-Verlag
Abstract

Caching Murphi 5.1 (Finite Horizon Probabilistic Murphi)

Caching Murphi 5.1 is a finite horizon probabilistic model checker with finite precision real numbers. Caching Murphi 5.1 is described in the following paper.

[DIMTZ03]
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli,
Finite Horizon Analysis of Markov Chains with the Murphi Verifier,
Proceedings of: 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME), 21-24 October 2003, L'Aquila (Italy), LNCS, Springer-Verlag
Co-sponsored by the IFIP TC10/WG10.5 Working Group on: Design and Engineering of Electronic Systems
Abstract

Caching Murphi 5.2 (Finite Horizon Probabilistic Murphi)

Caching Murphi 5.2 is a finite horizon probabilistic model checker with finite precision real numbers. Cmurphi 5.2 can handle all BPCTL formulas and works using a dfs rather than a bfs as in CMurphi 5.1

CMurphi 5.2 is described in the following paper:

[DIMTZ04]
Giuseppe Della Penna, Benedetto Intrigila, Igor Melatti, Enrico Tronci, Marisa Venturini Zilli,
Bounded Probabilistic Model Checking with the Murphi Verifier ,
Proceedings of: Formal Methods in Computer-Aided Design: 5th International Confrence, FMCAD 2004, Austin, Texas, USA, November 15-17, 2004 LNCS 3312, Springer-Verlag
Abstract

Caching Murphi Download

From here you can download caching murphi source code

Finite Horizon Probabilistic Murphi Download

Some Protocol

Here are some of the protocols we tried out with cached murphi.

Protocol table .

More on Cached Murphi

More online info on cached murphi can be found here