Difference between revisions of "Publications/hamez.07.pohll"
From LRDE
(Created page with "{{Publication | date = 2007-01-01 | authors = Alexandre Hamez, Fabrice Kordon, Yann Thierry-Mieg | title = libDMC: a library to Operate Efficient Distributed Model Checking | ...") |
|||
Line 7: | Line 7: | ||
| urllrde = 200703-POHLL |
| urllrde = 200703-POHLL |
||
| 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. |
| 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. |
||
+ | | lrdepaper = http://www.lrde.epita.fr/dload/papers/hamez.07.pohll.pdf |
||
| type = inproceedings |
| type = inproceedings |
||
| id = hamez.07.pohll |
| id = hamez.07.pohll |
Revision as of 16:42, 22 October 2013
- 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
- Date
- 2007-01-01
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
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, project = {Verification}, 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.} }