In June 2002, he obtained the Master of Science degree (Diplôme d'Etudes Approfondies) in Computer Science from the
University Joseph Fourier - Grenoble 1 (France). His research was carried out at
INRIA Rhône-Alpes (France) in the
VASY team, where he worked on the massively parallel generation of very large transition systems, and the design of version V3 of DISTRIBUTOR currently part of
CADP toolbox. Christophe's Master of Science was funded by a
university merit grant according to academic honors and by
INRIA.
From October 2002 to December 2005, Christophe worked at
INRIA Rhône-Alpes (France) in the
VASY team on a distributed verification engine based on Boolean Equation Systems and its applications to explicit-state verification problems.
This work ended up with the definition and development of two distributed-memory algorithms, DSOLVE and MB-DSOLVE, using clusters of PCs connected by TCP/IP sockets.
He employed its distributed algorithms as computing engine for three on-the-fly verification tools developed within the
CADP toolbox using the OPEN/CAESAR environment: the Bisimulator equivalence checker, the Tau_Confluence reductor, and the Evaluator model checker.
Experimental measures performed on clusters of machines showed quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.
He also was one of the main designers and developers of the sequential and distributed version of the Extractor test-case generator giving an encoding of the problem in terms of local boolean equation system resolution with diagnostic.
In January 2006, Christophe Joubert was laureate of a
Lavoisier grant from the French Ministry of Foreign Affairs. He joined the
GISUM group at the
University of Malaga (Spain) and worked, within the
SELF project, on using abstraction and static analysis to reduce a program state space when realizing on-the-fly explicit-state verification. He applied his knowledge of model checking and boolean equation systems to provide new encodings of static analyses and to connect the
C.OPEN compiler to the
CADP toolbox.