PReach: A Distributed Explicit State Model Checker

We present PReach, a distributed explicit state model checker based on Murphi. PReach is implemented in the concurrent functional language Erlang. This allowed a clean and simple implementation, with the core algorithms under 1000 lines of code. Additionally, the PReach implementation is targeted to deal with very large models. PReach is able to check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published to date for a distributed explicit state model checker.