libDMC: a library to Operate Efficient Distributed Model Checking

Alexandre Hamez 1 Fabrice Kordon 1 Yann Thierry-Mieg 1
1 MoVe - Modélisation et Vérification
LIP6 - Laboratoire d'Informatique de Paris 6
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 multithreaded 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.
Type de document :
Communication dans un congrès
Workshop on Performance Optimization for High-Level Languages and Libraries - associated to IPDPS'2007, Mar 2007, Long Beach, California, United States. Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, 2007, 〈10.1109/IPDPS.2007.370647〉
Liste complète des métadonnées
https://hal.inria.fr/hal-00687573
Contributeur : Ist Rennes <>
Soumis le : vendredi 13 avril 2012 - 15:17:59
Dernière modification le : mercredi 21 mars 2018 - 18:58:11

Identifiants

Collections

GRID5000 | UPMC | LIP6

Citation

Alexandre Hamez, Fabrice Kordon, Yann Thierry-Mieg. libDMC: a library to Operate Efficient Distributed Model Checking. Workshop on Performance Optimization for High-Level Languages and Libraries - associated to IPDPS'2007, Mar 2007, Long Beach, California, United States. Parallel and Distributed Processing Symposium, 2007. IPDPS 2007. IEEE International, 2007, 〈10.1109/IPDPS.2007.370647〉. 〈hal-00687573〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

265

Contact


archive-ouverte@inria.fr