Murphi

Murphi Model Checker. The Murphi tool was originally developed by Professor David Dill’s group at Stanford. It is an enumerative (explicit state) model checker, with its own input language (also called Murphi) which is a guard -> action notation similar to Unity, which are repeatedely executed in an infinite loop. The Murphi language contains support for familiar data types for programmers (subranges, enumerated types, arrays, and records), as well as more advanced types such as the multiset, or scalarset. Murphi has a formal verifier that is based on explicit state enumeration, which can be performed as a depth-first or breadth-first search of the state space. States encountered in this mode are saved in a hash table. States generated that exist in the hash table are not expanded. Murphi is still widely used, especially by the Microprocessor industry, to verify cache coherence protocols. Many versions of Murphi have since been developed both by this group and others. This page contains a description of the various versions of Murphi that have been developed over the years as well as download links. The version of Murphi described herein may have slightly altered functionality than the desription above, which mainly describes the original (standard) Murphi.


References in zbMATH (referenced in 16 articles )

Showing results 1 to 16 of 16.
Sorted by year (citations)

  1. Zhang, Nan; Duan, Zhenhua; Tian, Cong; Du, Hongwei: A novel approach to verifying context free properties of programs (2020)
  2. Jančík, Pavel; Kofroň, Jan: On partial state matching (2017)
  3. Evangelista, Sami; Kristensen, Lars Michael: Dynamic state space partitioning for external memory state space exploration (2013) ioport
  4. Jensen, Kurt; Kristensen, Lars M.; Mailund, Thomas: The sweep-line state space exploration method (2012)
  5. Edelkamp, S.; Sulewski, D.; Barnat, J.; Brim, L.; Šimeček, P.: Flash memory efficient LTL model checking (2011)
  6. Chen, Xiaofang; Yang, Yu; Gopalakrishnan, Ganesh; Chou, Ching-Tsun: Efficient methods for formally verifying safety properties of hierarchical cache coherence protocols (2010)
  7. Evangelista, Sami; Pajault, Christophe: Solving the ignoring problem for partial order reduction (2010) ioport
  8. Edelkamp, Stefan; Jabbar, Shahid; Sulewski, Damian: Distributed verification of multi-threaded C++ programs (2008)
  9. Holzmann, Gerard J.: A stack-slicing algorithm for multi-core model checking (2008)
  10. Pelánek, Radek: Properties of state spaces and their applications (2008) ioport
  11. Veanes, Margus; Ernits, Juhan; Campbell, Colin: State isomorphism in model programs with abstract data structures (2007)
  12. Ganai, Malay K.; Gupta, Aarti; Yang, Zijiang; Ashar, Pranav: Efficient distributed SAT and sAT-based distributed bounded model checking (2006) ioport
  13. Garavel, Hubert; Serwe, Wendelin: State space reduction for process algebra specifications (2006)
  14. Grumberg, Orna; Heyman, Tamir; Schuster, Assaf: A work-efficient distributed algorithm for reachability analysis (2006)
  15. Adi, Kamel; Debbabi, Mourad; Me Jri, Mohamed: A new logic for electronic commerce protocols (2003)
  16. Ben-David, Shoham; Grumberg, Orna; Heyman, Tamir; Schuster, Assaf: Scalable distributed on-the-fly symbolic model checking (2003) ioport