Description:

The VASY team of INRIA Rhône-Alpes works in the field of formal specification and verification of critical systems. The research activities of VASY encompass both theoretical aspects related to the definition of formal specification languages and their associated verification techniques, and also practical aspects related to the development of software tools assisting the design process. The main software contribution of VASY is CADP, a verification toolbox that offers a complete range of functionalities for designing critical systems: compilation and rapid prototyping, interactive and guided simulation, random execution, equivalence checking, model checking, and test case generation. To deal with large systems, CADP also features sophisticated analysis techniques, such as on-the-fly, compositional, and distributed verification. CADP was applied to numerous industrial case-studies and its various generic software components were used to build other research tools.

The HELIX team of INRIA Rhône-Alpes works in the field of bioinformatics and system biology. One of the research activities of HELIX concerns the modelling and analysis of genetic regulatory networks (GRNs), the results of which can offer useful predictions in complement to the experimental data available. The method employed is based upon describing the dynamic behaviour of GRNs as systems of piecewise-linear differential equations, building a discrete abstraction of these systems that preserves the qualitative dynamic behaviour, and analysing it using model checking techniques. This method underlies the GNA tool developed by HELIX. Recent work [BBJ+04,BRJ+05] demonstrated that the coupling between GNA and CADP allows to analyse GRNs effectively by applying state space minimization and model checking of branching-time logics.

This post-doc fellowship is funded by the project "EC-MOAN: Scalable modeling and analysis techniques to study emergent cell behavior: Understanding the E. coli stress response", which is funded by the European Commission (6FP, NEST Pathfinder) and will start in February 2007. Besides INRIA Rhône-Alpes, other participants in EC-MOAN include biologists, computer scientists, and mathematicians from the Université Joseph Fourier (UJF) in Grenoble, the Vrije Universiteit (VU) in Amsterdam, the Centrum voor Wiskunde and Informatica (CWI) in Amsterdam, the University of Edinburgh, and the Masaryk University in Brno. The objective of EC-MOAN is to develop new, scalable methods for the modeling and analysis of integrated genetic, metabolic, and signaling networks, and applying these methods to enhance our understanding of a bacterial model system.

The mathematical models of biological systems developed within EC-MOAN will be amenable to automated analysis by a sequence of transformations leading to large state transition graphs. Biologically-relevant properties will be characterized using appropriate extensions of temporal logics and will be evaluated on these graphs by using sequential and distributed model checking algorithms. The results of these analyses will be compared with the biological experiments and will serve to predict the behaviour of the bacterial system considered and to finely tune the mathematical models proposed in the project.

The research work and expected results of the post-doc are the following:

• Design and implement sequential model checking algorithms for the extended temporal logics defined within the project. These logics are targeted to the description of biologically-relevant properties of genetic regulatory networks.


• Propose and develop distributed versions of the model checking algorithms, which are able to use the resources of several machines connected by a network. The goal of this activity is to scale up the capabilities of model checking in order to handle large systems.


• Experiment the proposed sequential and distributed algorithms on the state-transition models generated from biological systems within the project. The benchmark information obtained should be used for finely tuning the performance of the algorithms.

We are looking for a candidate owning a PhD in computer science and having a strong experience in formal methods, particularly in the field of model checking. Additional experience in parallel and distributed programming would be welcome. The candidate should be able to work in a multidisciplinary research environment.

Application:

Candidates should send their applications by e-mail to Radu.Mateescu@inria.fr. Applications should consist of:

• A motivation letter


• A detailed Curriculum Vitae with publication list


• An electronic copy of (or web link to) the PhD thesis


• Recommendations from senior scientists

The deadline for applications is January 20, 2007.

The post-doc will start in February 2007 and will have a duration of three years. It will be based in Dijon (France) at the LE2I laboratory.

Contact:

Radu Mateescu
INRIA Rhône-Alpes / VASY
Inovallée
655, avenue de l'Europe
F-38330 Montbonnot St Martin
France
E-mail: Radu.Mateescu@inria.fr

References:

• [BBJ+04] Grégory Batt, Damien Bergamini, Hidde de Jong, Hubert Garavel, and Radu Mateescu. Model Checking Genetic Regulatory Networks using GNA and CADP. Proceedings of the 11th International SPIN Workshop on Model Checking of Software SPIN'2004 (Barcelona, Spain), Lecture Notes in Computer Science vol. 2989, pp. 156-161. Springer Verlag, April 2004.


• [BRJ+05] Grégory Batt, Delphine Ropers, Hidde de Jong, Johannes Geiselmann, Radu Mateescu, Michel Page, and Dominique Schneider. Validation of Qualitative Models of Genetic Regulatory Networks by Model Checking: Analysis of the Nutritional Stress Response in Escherichia Coli. Bioinformatics 21 (suppl. 1):i19-i28, 2005.


• [GMS01] Hubert Garavel, Radu Mateescu, and Irina Smarandache. Parallel State Space Construction for Model-Checking. Proceedings of the 8th International SPIN Workshop on Model Checking of Software SPIN'2001 (Toronto, Canada), Lecture Notes in Computer Science vol. 2057, pp. 217-234. Springer Verlag, May 2001. Revised version available as INRIA Research Report RR-4341 (December 2001).


• [GMB+06] Hubert Garavel, Radu Mateescu, Damien Bergamini, Adrian Curic, Nicolas Descoubes, Christophe Joubert, Irina Smarandache-Sturm, and Gilles Stragier. DISTRIBUTOR and BCG_MERGE: Tools for Distributed Explicit State Space Generation. Proceedings of the 12th International Conference on Tools and Algorithms for the Construction and Analysis of Systems TACAS'2006 (Vienna, Austria), Lecture Notes in Computer Science vol. 3920, pp. 445-449. Springer Verlag, March-April 2006.


• [MS03] Radu Mateescu and Mihaela Sighireanu. Efficient On-the-Fly Model Checking for Regular Alternation-Free Mu-Calculus. Science of Computer Programming 46(3):255-281, March 2003.

Back to the VASY Home Page