Open Collections

Abstract

PReach, developed at the University of British Columbia and Intel, is a state of the art parallel model checker. However, like many model checkers, it faces reliability problems. A single crash causes the loss of all progress in checking a model. For computations that can take days, restarting from the beginning is a problem. To solve this, we have developed PReachDB, a modified version of PReach. PReachDB maintains the state of the model checking computation even across program crashes by storing key data structures in a database. PReachDB uses the Mnesia distributed database management system for Erlang. PReachDB replicates data to allow the continuation of the computation after a node failure. This project provides a proof-of-concept implementation with performance measurements.