Technical Reports

The ICICS/CS Reading Room

UBC CS TR-2010-05 Summary

PReach: A Distributed Explicit State Model Checker, April 06, 2010 Flavio M. de Paula, Brad Bingham, Jesse Bingham, John Erickson, Mark Reitblatt and Gaurav Singh, 4 pages

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.

If you have any questions or comments regarding this page please send mail to