Christophe Joubert

Christophe JOUBERT

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

Biographical Notes

In 2001, Christophe Joubert carried out a research training (four months) at the Department of Computer Science, University of California Santa Barbara (USA), on the integration of shape analysis, a static computation of program memory configuration topology, into Action Language Verifier. Christophe's research training was funded by the Rhône-Alpes region grant under the Education Abroad Program.
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.
During the same year, Christophe Joubert graduated in September with a diploma of Magister in Computer Science (Magistère d'Informatique) at the University Joseph Fourier - Grenoble 1 (France). His research training (four months) was carried out in the Netherlands, at the Formal Methods and Tools group of the University of Twente, Enschede, on a set of performance and dependability analysis components for CADP. This research work was founded by an Isère department grant and by AMETIST project.
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.
Christophe obtained his Ph.D. Thesis in Computer Science from the Grenoble Institute of Technology (INPG) (France) in December 2005 with a thesis entitled "Distributed On-the-Fly Verification of Large State Spaces". His Ph.D. grant was funded by the French Ministry of Education and Research.
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.
In February 2007, he obtained a research position at the Technical University of Valencia (UPV) (Spain), under a Juan de la Cierva contract. Now, he is working on formal methods and model checking at the Computer Science Department (DSIC) in the ELP team. Christophe's present activities are described on his personal page at UPV.


Valid XHTML 1.0!

Last modification : 07/02/23 16:57:37

Valid CSS!