libDMC: a library to Operate Efficient Distributed Model Checking

Authors

Alexandre Hamez, Fabrice Kordon, Yann Thierry-Mieg

Where

Workshop on Performance Optimization for High-Level Languages and Libraries — associated to IPDPS'2007

Type

inproceedings

Projects

Verification"Verification" is not in the list (Vaucanson, Spot, URBI, Olena, APMC, Tiger, Climb, Speaker ID, Transformers, Bison, ...) of allowed values for the "Related project" property.

Date

2007-03-13

Abstract

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.

Documents

• Paper

Bibtex (lrde.bib)

@InProceedings{	  hamez.07.pohll,
  author	= {Alexandre Hamez and Fabrice Kordon and Yann Thierry-Mieg},
  title		= {{libDMC}: a library to Operate Efficient Distributed Model
		  Checking},
  booktitle	= {Workshop on Performance Optimization for High-Level
		  Languages and Libraries --- associated to IPDPS'2007},
  year		= 2007,
  abstract	= {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.}
}