current activity 01/2006 - onwards
So far, my work can be divided in two parts: static analysis applications using a Boolean Equation System verification engine and description of new static analyses to further reduce a program explicit state space.
If you want more information, check out the presentation slide I made for the ISOLA'06 symposium (Nov 2006).
You may also consult my list of publications for further information.
Hereafter is a small description of my current research project:
- place:
- University of Málaga, LCC department, GISUM group, FMSE project, Málaga (Spain)
- title:
- static analyses using (parameterised) boolean equation systems
- domain:
- formal verification and reduction methods
- collaborators:
- Pedro Merino and María del Mar Gallardo
- funding:
- Lavoisier grant from the French ministry of foreign affairs
- project:
- research work part of Software Engineering and Lightweight Formalisms (SELF) research project of the Spanish Program of Computer Science Technology (TIN) number 2004-7943-C04-01, module M-1.3: Property analysis of systems based on components
- abstract:
- Static analysis, model checking and abstract interpretation are verification techniques that everyone is willing to combine to scale up the size of currently verifiable systems. In this paper, we detail a generic approach to solve classical data flow analyses using the resolution of boolean equation systems (BESs). The input program is abstracted into an implicit labeled transition system (LTS), being independent from the program specification language, which allows an on-the-fly static analysis of the program. Moreover, using implicit BESs as an intermediate representation enabled us to reformulate principal data flow analyses encountered in the literature, which were previously encoded in terms of mu-calculus formulas with forward and backward modalities. Our work has been implemented and integrated into the widespread verification platform CADP, and experimented on real examples.
- keywords:
- boolean equation systems, data flow analysis, on-the-fly verification, labeled transition systems, model checking
- publication:
- Gallardo - et - al - ISOLA - 06
- Gallardo - et - al - 06
- talk:
- Joubert - GISUM - 05
- tool:
- ANNOTATOR
past activities
distributed model checking 10/2002 - 12/2005
- place:
- INRIA, Rhône-Alpes research unit, VASY project, Grenoble (France)
- position:
- Ph.D. student/researcher
- title:
- Distributed On-the-Fly Verification of Large State Spaces
- domain:
- formal verification methods and distributed algorithms
- advisors:
- Hubert Garavel (director) and Radu Mateescu (scientific advisor)
- funding:
- french research ministry grant
- project:
- research work part of Standard Process Algebra Research and Tools SENVA, Associated Team INRIA program between INRIA/VASY and CWI/SEN, section distributed algorithms for the verification of finite-state systems
- abstract:
-
The verification of concurrent finite-state systems is confronted in practice with the state explosion problem (prohibitive size of the underlying state space), which occurs for realistic systems containing many parallel processes and complex data structures. Various techniques for fighting against state explosion have been proposed, such as on-the-fly verification, partial order reduction, and distributed verification. However, practical experience has shown that none of these techniques alone is always sufficient to handle large-scale systems.
In this thesis, we propose a combination of these approaches in order to scale up their capabilities. Our approach is based upon Boolean Equation Systems (BESs), which provide an elegant intermediate representation for verification problems defined on Labeled Transition Systems, such as equivalence checking, tau-confluence reduction, model checking of alternation-free mu-calculus, and test-case generation.
We propose DSolve (Joubert - Mateescu - PDP - 05) and MB-DSolve (Joubert - Mateescu - SPIN - 06), two new algorithms for distributed on-the-fly resolution of BESs (containing one, resp. several equation blocks), and employ them as computing engines for four on-the-fly verification tools developed within the CADP toolbox using the OPEN/CAESARenvironment: the BISIMULATOR equivalence checker (Joubert - Mateescu - PDMC - 04, Bergamini - et - al - TACAS - 05 - a), the TAU_CONFLUENCE reductor, the EVALUATOR model checker (Joubert - Mateescu - SPIN - 06), and the EXTRACTOR test-case generator (Joubert - Mateescu - SPIN - 06). Experimental measures performed on clusters of machines show quasi-linear speedups and a good scalability of the distributed versions of these tools w.r.t. their sequential counterparts.
- keywords:
- boolean equation systems, distributed memory algorithm, on-the-fly verification, equivalence checking, partial order reduction, model checking, test case generation
- publication:
- Joubert - 05 (also on VASY website, INRIA open archives, and CNRS open archives)
- Joubert - Mateescu - SPIN - 06
- Joubert - Mateescu - 06
- Bergamini - et - al - TACAS - 05 - a
- Bergamini - et - al - TACAS - 05 - a
- Joubert - Mateescu - PDP - 05
- Joubert - Mateescu - PDMC - 04
- Joubert - PDMC - 03
- talk:
- Joubert - GISUM - 05
- Joubert - SENVA - GRID - 05
- Joubert - SENVA - 05
- Joubert - ELP - 05
- Joubert - MSTII - 04
- Joubert - SENVA - 04
- Joubert - EJCP - 03
- tool demonstration:
- Bergamini - et - al - TACAS - 05 - b
performance evaluation 06/2002 - 09/2002
- place:
- Department of computer science, Universiteit Twente, FMT group, Enschede (Holland)
- position:
- visiting scientist
- title:
- a set of performance and dependability analysis components for CADP
- domain:
- formal verification methods
- advisors:
- Ed Brinksma (director) and Holger Hermanns (scientific advisor)
- funding:
- Isère department grant
- project:
- research work part of Advanced Methods for Timed Systems AMETIST, european project IST-2001-35304, EC 5th Framework Program, section analysis and tools: stochastic techniques
- abstract:
- This work aimed at designing 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, state space, steady state and transient analysis, on-the-fly elimination of non-determinism for stochastic systems
- publication:
- Hermanns - Joubert - TACAS - 03 - a
- tool demonstration:
- Hermanns - Joubert - TACAS - 03 - b
parallel generation 10/2001 - 06/2002
- place:
- INRIA, Rhône-Alpes research unit, VASY project, Grenoble (France)
- position:
- master student
- title:
- massively parallel generation of very large transition systems
- domain:
- formal methods
- advisors:
- Hubert Garavel (director) and Radu Mateescu (scientific advisor)
- funding:
- merit grant according to academic honors
- project:
- research work part of Architecture Evolvable Software ARCHWARE, european project IST-2001-32360, EC 5th Framework Program, section description and verification of functional properties
- abstract:
- 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:
- state space, on-the-fly generation, distributed memory algorithm, partitioned LTS
- publication:
- Garavel - et - al - TACAS - 06 - a
- Joubert - MASTER - 02
- talk:
- Joubert - VASY - 02 - c
- tool demonstration:
- Garavel - et - al - TACAS - 06 - b
- Garavel - et - al - PDMC - 05
shape analysis 04/2001 - 07/2001
- place:
- Department of computer science, University of California, Santa Barbara (USA)
- position:
- bachelor student
- title:
- integrating shape analysis, a static computation of program memory configuration topology, into Action Language Verifier
- domain:
- formal verification methods
- advisors:
- Saddek Bensalem (director) and Tevfik Bultan (scientific advisor)
- funding:
- Rhône-Alpes region grant
- keywords:
- shape analysis, static analysis, infinite state symbolic model
multi-agent systems 11/1999 - 07/2000
- place:
- IMAG, LEIBNIZ laboratory, MAGMA project, Grenoble (France)
- position:
- licence student
- title:
- a communication model for multi-agent systems in the context of ROBOCUP simulation
- advisors:
- Yves Demazeau (director) and Christof Baeijs (scientific advisor)
- keywords:
- cooperation, communication, ROBOCUP simulation, AEIO model
