A. Hamez and F. Kordon and Y. Thierry-Mieg.
libDMC: a library to Operate Efficient Distributed Model Checking.
Workshop on Performance Optimization for High-Level Languages and Libraries (POHLL) - associated to IPDPS'2007 POHLL07 Long Beach, California, USA 30 March 2007
Model checking is a formal verification technique that allows to automatically prove that a system's behavior is
correct. However it is often prohibitively expensive in time and memory complexity, due to the so-called state
space explosion problem. We present a generic multi-threaded and distributed infrastructure library designed to
allow distribution of the model checking procedure over a cluster of machines. This library is generic, and is
designed to allow encapsulation of any model checker in order to make it distributed. Performance evaluations are
reported and clearly show the advantages of multi-threading to occupy processors while waiting for the network,
with linear speedup over the number of processors.
to top