The new address of Christophe Joubert's home page is:

http://www.dsic.upv.es/~joubert

P ublications

All articles are available from the VASY (Validation of Systems) project website of INRIA Rhône-Alpes research unit (The French National Institute for Research in Computer Science and Control).

If you cannot find them, send me a mail and you'll be enlightened.

list of publications

Refereed International Conference Papers:

[Bergamini - et - al - TACAS - 05 - a]
Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland), Apr 2005.
[Joubert - Mateescu - PDP - 05]
Christophe Joubert and Radu Mateescu. Distributed Local Resolution of Boolean Equation Systems. Euromicro Conference on Parallel, Distributed and Network based Processing, PDP'05 (Lugano, Switzerland), Feb 2005.
[Hermanns - Joubert - TACAS - 03 - a]
Holger Hermanns and Christophe Joubert. A Set of Performance and Dependability Analysis Components for CADP. Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland), Apr 2003.

Refereed International Workshop Papers:

[Joubert - Mateescu - PDMC - 04]
Christophe Joubert and Radu Mateescu. Distributed On-the-Fly Equivalence Checking. International Workshop on Parallel and Distributed Methods in Verification PDMC'2004 (London, UK), Sep 2004.
[Joubert - PDMC - 03]
Christophe Joubert. Distributed Model Checking: From Abstract Algorithms to Concrete Implementations. International Workshop on Parallel and Distributed Model Checking PDMC'2003 (Boulder, Colorado, USA), Jul 2003.

Research Reports:

[Joubert - MASTER - 02]
Christophe Joubert. Techniques et outils pour la construction massivement parallèle de systèmes de transitions. Institut National Polytechnique de Grenoble et Université Joseph Fourier (Grenoble, France), Jun 2002.

International and National Talks:

[Joubert - MSTII - 04]
Christophe Joubert. Analyse d'espaces d'états par résolution distribuée de systèmes d'équations booléennes. Journée des doctorants de l'Ecole Doctorale de Mathématiques, Sciences et Technologies de l'Information, Informatique MSTII'2004 (Grenoble, France), Nov 2004.
[Joubert - SENVA - 04]
Christophe Joubert. Distributed Local Resolution of Boolean Equation Systems for Distributed On-the-Fly Equivalence Checking. International Workshop on System Engineering and Validation SENVA'2004 (Allevard-les-Bains, France), Jun 2004.
[Joubert - VASY - 03]
Christophe Joubert. Combiner vérification compositionnelle et évaluation de performances dans CADP. Séminaire annuel d'équipe VASY'2003 (Saint Pierre de Chartreuse, France), Jun 2003.
[Joubert - EJCP - 03]
Christophe Joubert. Approches massivement parallèles pour l'analyse de très grands espaces d'états. Ecole de Jeunes Chercheurs en Programmation EJCP'2003 (Aussois, France), Mai 2003.
[Joubert - VASY - 02 - a]
Christophe Joubert. Outils logiciels pour la combinaison de vérification fonctionnelle et d'évaluation de performances au sein de CADP. Séminaire annuel d'équipe VASY'2002 (Aix les Bains, France), Oct 2002.
[Joubert - VASY - 02 - b]
Christophe Joubert. Techniques et outils pour la construction massivement parallèle de systèmes de transitions. Séminaire annuel d'équipe VASY'2002 (Aix les Bains, France), Oct 2002.

Refereed International Tool Demonstration:

[Bergamini - et - al - TACAS - 05 - b]
Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu. BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking. Tool session of Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland), Apr 2005.
[Hermanns - Joubert - TACAS - 03 - b]
Holger Hermanns and Christophe Joubert. A Set of Performance and Dependability Analysis Components for CADP. Tool Session of Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland), Apr 2003.

Refereed International Conference Papers

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking

paper: (pdf) 2005

presentation: (pdf) 2005

(top)

by Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu.
BibTeX:
@inproceedings{Bergamini-Descoubes-Joubert-Mateescu-05-a,
author = {Damien Bergamini and Nicolas Descoubes and Christophe Joubert and Radu Mateescu},
title = {BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking},
booktitle = {Proceedings of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland)},
year = {2005},
editor = {Nicolas Halbwachs and Lenore Zuck},
publisher = {Springer Verlag},
series = {Lecture Notes in Computer Science},
volume = {3440},
pages = {581--585},
month = {April}
}

Distributed Local Resolution of Boolean Equation Systems

paper: (pdf) 2005

presentation: (pdf) 2005

(top)

by Christophe Joubert and Radu Mateescu.

Boolean Equation Systems (BESs) allow to represent various problems encountered in the area of propositional logic programming and verification of concurrent systems. Several sequential algorithms for global and local BES resolution have been proposed so far, mainly in the field of verification; however, these algorithms do not scale up satisfactorily as the size of BESs increases. In this paper, we propose a distributed algorithm, called DSOLVE, which performs the local resolution of a BES using a set of machines connected by a network. Our experiments for solving large BESs using clusters of PCs show linear speedups and a scalable behaviour of DSOLVE w.r.t. its sequential counterpart.

Keywords:
distributed memory algorithm, boolean equation systems, distributed termination detection, local resolution
BibTeX:
@inproceedings{Joubert-Mateescu-05,
author = {Christophe Joubert and Radu Mateescu},
title = {Distributed Local Resolution of Boolean Equation Systems},
booktitle = {Proceedings of the 13th Euromicro Conference on Parallel, Distributed and Network based Processing, PDP'05 (Lugano, Switzerland)},
publisher = {IEEE Computer Society Press},
year = {2005}
month = {February}
}

A Set of Performance and Dependability Analysis Components for CADP

paper: (pdf) 2003

presentation: (pdf) 2003

(top)

by Holger Hermanns and Christophe Joubert.

This paper describes a set of analysis components that open the way to perform performance and dependability analysis with the CADP toolbox, originally designed for verifying the functional correctness of LOTOS specifications. Three new tools (named BCG_STEADY, BCG_TRANSIENT, and DETERMINATOR) have been added to the toolbox. The approach taken fits well within the existing architecture of CADP, which doesn't need to be altered to enable performance evaluation.

Keywords:
performance evaluation, functional verification, steady-state and transient analysis, non-determinism reduction
BibTeX:
@inproceedings{Hermanns-Joubert-03-a,
author = {Holger Hermanns and Christophe Joubert},
title = {A Set of Performance and Dependability Analysis Components for CADP},
booktitle = {Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland)},
year = {2003},
editor = {Hubert Garavel and John Hatcliff},
publisher = {Springer Verlag},
series = {Lecture Notes in Computer Science},
volume = {2619},
pages = {425--430},
month = {April}
}

Refereed International Workshop Papers

Distributed On-the-Fly Equivalence Checking

paper: (pdf) 2004

presentation: (pdf) 2004

(top)

by Christophe Joubert and Radu Mateescu.

On-the-fly equivalence checking consists in comparing two Labeled Transition Systems (LTSs) modulo a given equivalence relation by exploring them in a demand-driven way. Since it avoids the explicit construction of LTSs, this method is able to detect errors even in systems that are too large to fit in the memory of a computer. In this paper, we aim at further improving the performance of on-the-fly equivalence checking using several machines connected by a network. We propose DSOLVE, a new algorithm for distributed on-the-fly resolution of Boolean Equation Systems (BESs), which enables equivalence checking modulo various relations characterized in terms of BESs. DSOLVE serves as verification engine for the distributed version of BISIMULATOR, an on-the-fly equivalence checker developed within the CADP verification toolbox using the OPENCAESAR environment. Our experimental measures show quasi-linear speedups and a good scalability of the distributed version of BISIMULATOR w.r.t. its sequential version.

Keywords:
bisimulation, boolean equation system, distributed memory algorithm, equivalence checking, distributed termination detection, cluster of machines
BibTeX:
@inproceedings{Joubert-Mateescu-04,
author = {Christophe Joubert and Radu Mateescu},
title = {Distributed On-the-Fly Equivalence Checking},
booktitle = {Proceedings of the 3rd International Workshop on Parallel and Distributed Methods in Verification PDMC'2004 (London, UK)},
year = {2004},
editor = {Lubos Brim and Martin Leucker},
series = {Electronic Notes in Theoretical Computer Science},
volume = {128},
issue = {3},
pages = {47--62},
publisher = {Elsevier}
}

Distributed Model Checking: From Abstract Algorithms to Concrete Implementations

paper: (pdf) 2003

presentation: (pdf) 2003

(top)

by Christophe Joubert.

Distributed Model Checking (DMC) is based on several distributed algorithms, which are often complex and error prone. In this paper, we consider one fundamental aspect of DMC design: message passing communication, the implementation of which presents hidden tradeoffs often dismissed in DMC related literature. We show that, due to such communication models, high level abstract DMC algorithms might face implicit pitfalls when implemented concretely. We illustrate our discussion with a generic distributed state space generation algorithm.

Keywords:
distributed model checking, distributed memory algorithm, message passing, cluster of machines
BibTeX:
@inproceedings{Joubert-03,
author = {Christophe Joubert},
title = {Distributed Model Checking: From Abstract Algorithms to Concrete Implementations},
booktitle = {Proceedings of the 2nd International Workshop on Parallel and Distributed Model Checking PDMC'2003 (Boulder, Colorado, USA)},
year = {2003},
editor = {Lubos Brim and Orna Grumberg},
series = {Electronic Notes in Theoretical Computer Science},
volume = {89},
issue = {1},
publisher = {Elsevier}
}

Research Reports

Techniques et outils pour la construction massivement parallèle de systèmes de transitions

(top)

by Christophe Joubert.

This master research work aimed at designing and implementing new algorithms for the massively parallel generation of large transition systems problem, in order to prepare distributed model checking. We gave a complete state of the art of research works on parallel generation of models. Then, we proposed a new algorithm for the parallel construction of models obtained from programs described with high level languages, such as LOTOS. One novel aspect of our approach is the distributed management of dynamic data structures (lists, trees, etc.) between several machines. We also specified our algorithm in LOTOS and verified its functional properties (absence of deadlock, termination detection, safety) by mean of the CADP toolbox. A prototype implementation of our algorithm has been implemented in DISTRIBUTOR tool of CADP. The experiments on a cluster of PCs confirmed the good behavior of our algorithm and showed important performance gain in memory and time execution.

Keywords:
on-the-fly generation, distributed memory algorithm, partitioned labelled transition systems, dynamic data structure, distributed termination detection, cluster of machines
BibTeX:
@mastersthesis{Joubert-02-a,
author = {Christophe Joubert},
title = {Techniques et outils pour la construction massivement parallèle de systèmes de transitions},
school = {Institut National Polytechnique de Grenoble et Université Joseph Fourier},
year = {2002}
type = {Mémoire de DEA en informatique},
address = {Grenoble},
month = jun
}

International and National Talks

Analyse d'espaces d'états par résolution distribuée de systèmes d'équations booléennes

presentation: (pdf) 2004

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-04-b,
author = {Christophe Joubert},
title = {Analyse d'espaces d'états par résolution distribuée de systèmes d'équations booléennes},
howpublished = {Journée des doctorants de l'Ecole Doctorale de Mathématiques, Sciences et Technologies de l'Information, Informatique MSTII'2004 (Grenoble, France)},
month = {November},
year = {2004}
}

Distributed Local Resolution of Boolean Equation Systems for Distributed On-the-Fly Equivalence Checking

presentation: (pdf) 2004

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-04-a,
author = {Christophe Joubert},
title = {Distributed Local Resolution of Boolean Equation Systems for Distributed On-the-Fly Equivalence Checking},
howpublished = {1st International Workshop on System Engineering and Validation SENVA'2004 (Allevard-les-Bains, France)},
month = {June},
year = {2004}
}

Combiner vérification compositionnelle et évaluation de performances dans CADP

presentation: (pdf) 2003

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-03-b,
author = {Christophe Joubert},
title = {Combiner vérification compositionnelle et évaluation de performances dans CADP},
howpublished = {Séminaire annuel d'équipe VASY'2003 (Saint Pierre de Chartreuse, France)},
month = {June},
year = {2003}
}

Approches massivement parallèles pour l'analyse de très grands espaces d'états

presentation: (pdf) 2003

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-03-a,
author = {Christophe Joubert},
title = {Approches massivement parallèles pour l'analyse de très grands espaces d'états},
howpublished = {Ecole de Jeunes Chercheurs en Programmation EJCP'2003 (Aussois, France)},
month = {May},
year = {2003}
}

Outils logiciels pour la combinaison de vérification fonctionnelle et d'évaluation de performances au sein de CADP

presentation: (pdf) 2002

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-02-b,
author = {Christophe Joubert},
title = {Outils logiciels pour la combinaison de vérification fonctionnelle et d'évaluation de performances au sein de CADP},
howpublished = {Séminaire annuel d'équipe VASY'2002 (Aix les Bains, France)},
month = {October},
year = {2002}
}

Outils logiciels pour la combinaison de vérification fonctionnelle et d'évaluation de performances au sein de CADP

presentation: (pdf) 2002

(top)

by Christophe Joubert.
BibTeX:
@misc{Joubert-02-c,
author = {Christophe Joubert},
title = {Techniques et outils pour la construction massivement parallèle de systèmes de transitions},
howpublished = {Séminaire annuel d'équipe VASY'2002 (Aix les Bains, France)},
month = {October},
year = {2002}
}

Refereed International Tool Demonstrations

BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking

2005

(top)

by Damien Bergamini, Nicolas Descoubes, Christophe Joubert and Radu Mateescu.
BibTeX:
@misc{Bergamini-Descoubes-Joubert-Mateescu-05-b,
author = {Damien Bergamini and Nicolas Descoubes and Christophe Joubert and Radu Mateescu},
title = {BISIMULATOR: A Modular Tool for On-the-Fly Equivalence Checking},
howpublished = {Tool Session of the 11th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2005 (Edinburgh, Scotland)},
year = {2005},
month = {April}
}

A Set of Performance and Dependability Analysis Components for CADP

2003

(top)

by Holger Hermanns and Christophe Joubert.
BibTeX:
@misc{Hermanns-Joubert-03-b,
author = {Holger Hermanns and Christophe Joubert},
title = {A Set of Performance and Dependability Analysis Components for CADP},
howpublished = {Tool Session of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2003 (Warsaw, Poland)},
year = {2003},
month = {April}
}
Valid XHTML 1.0!
Christophe.Joubert@inrialpes.fr

Last modification : 05/04/27 15:38:37

Valid CSS!