PReach (Parallel Reachability)

An industrial strength distributed explicit state model checker based on Murφ . The goal of this project was to develop a reliable, easy to maintain, scalable model checker that was compatible with the Murφ specification language. PREACH is implemented in the concurrent functional language Erlang, chosen for its parallel programming elegance. We use the original Murφ front-end to parse the model description, a layer written in Erlang to handle the communication aspects of the algorithm, and also use Murφ as a back-end for state expansion and to store the hash table. This allowed a clean and simple implementation, with the core parallel algorithms written in under 1000 lines of code. At Intel , we have used PReach to model check an industrial cache coherence protocol with approximately 30 billion states. To our knowledge, this is the largest number published for a distributed explicit state model checker. The latest (2011) cache coherence protocol verified with PReach at Intel approaches 100 billion states. PReach has been released to the public under an open source BSD license.

(Original) PReach Team

Brad Bingham (UBC)

Jesse Bingham (Intel)

Flavio M. de Paula (UBC)

John Erickson (Intel)

Gaurav Singh (Intel)

Mark Reitblatt (Cornell University)

PReach Source

The Preach Distribution site is the place to get the source code. Please read the License. Also, the README file contains the contact information specifically regarding releases.

PReach Literature and Other References

NOTE: This is a local copy. Originals are available from IEEE.

Industrial Strength Explicit State Model Checking, Brad Bingham, Jesse Bingham, Flavio M. de Paula, John Erickson, Gaurav Singh, Mark Reitblatt. 9th International Workshop on Parallel and Distributed Methods in Verification (PDMC'10), The Netherlands.

Presentation given by John Erickson at Galois Inc.

Discussion about PReach

Acknowledgments

I would like to acknowledge Prof. Mark Greenstreet (UBC) and Flemming Andersen (Intel) for their guidance and support, without which the success of this work would not be possible.