Beware! This job offer is no longer valid, the position has been fulfilled.

Logo Inria Logo CONVECS Logo LIG

The CONVECS team of Inria and LIG is recruiting a post-doc fellowship

Start date: January 1st, 2015

Type of contract: Fixed term contract (CDD) for 12 months.

Salary: About 2127 EUR net per month (2620 EUR gross), health insurance included (French Social Security system).

Location: This post-doctoral fellowship will be carried out at the Inria Montbonnot site, about 10 kilometres from Grenoble.

Subject: « Verification of Asynchronously Communicating Systems »


CONVECS is a research team of Inria and LIG. Its areas of expertise lie on formal verification techniques and tools for asynchronous concurrent systems. CONVECS is involved in several research directions: providing formal specification languages for describing concurrent systems; enhancing temporal logics and verification tools; fighting state explosion; designing generic components for verification, test, and performance evaluation; and demonstrating the applicability of its methods and tools on real-life applications with academic and industrial partnership. In particular, the members of CONVECS have been developing the CADP verification toolbox for about 20 years. CADP is dedicated to the design, analysis, and verification of asynchronous systems consisting of concurrent processes interacting via message passing.

Recent software is mostly constructed by reusing and composing existing components. Software components are usually stateful and therefore described using behavioral models such as finite state machines. Asynchronous communication is a classic interaction mechanism used for such software systems. However, analyzing communicating systems interacting asynchronously via reliable FIFO buffers is an undecidable problem. A typical approach is to check whether the system is bounded, and if not, the corresponding state space can be made finite by limiting the presence of communication cycles in behavioral models or by fixing buffer sizes.

In this line of work, we focus on infinite systems and we do not restrict the system by imposing any arbitrary bounds. We introduced recently a notion of stability and proved that once the system is stable for a specific buffer bound, it remains stable whatever larger bounds are chosen for buffers. This enables us to check certain properties on the system for that bound and to ensure that the system will preserve them whatever larger bounds are used for buffers. We also proved that computing this bound is undecidable but we are able to compute these bounds for many typical examples using heuristics and equivalence checking. The candidate will have to refine these results focusing on the perspectives of this work, to develop the corresponding tool support, and to apply these results to existing areas (e.g., cloud computing).

This post-doctoral fellowship will be part of the « OpenCloudware » project funded by the FSN (Fonds national pour la Société Numérique). The project is led by France Telecom / Orange Labs (Meylan, France) and involves 18 partners (among which Bull, Ow2, Thalès, Inria, etc.). OpenCloudware aims at providing an open software platform enabling the development, deployment, and administration of cloud applications. The verification techniques proposed in this project will be used for analyzing cloud applications developed in the context of OpenCloudware.

Work proposed and expected results: The candidate will complete the following tasks, among others:

Required skills and profile:


All questions concerning this post-doctoral fellowship should be addressed to:

Gwen Salaün
Inria Grenoble - Rhône-Alpes / CONVECS
655, avenue de l'Europe
38330 Montbonnot Saint-Martin
Tel : +33 (0)4 76 61 54 28
E-mail :

Application content:

Application submission:

Applications should be addressed directly to Gwen Salaün, preferably by e-mail, mentioning the position number #2014B. Applications received after October 10th, 2014 might not be considered if a candidate has been selected already.