Start date: September 1st, 2014

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: Inria Montbonnot site, about 10 kilometres from Grenoble

Subject: « Quantitative analysis of concurrent systems »

Objectives:

Asynchronous concurrent systems, which consist of several entities that execute independently and communicate by message-passing, are complex and difficult to analyze. Besides their functional correctness, quantitative analysis becomes increasingly important in order to estimate accurately, and reduce as much as possible, the energy consumption of these systems. To carry out such quantitative analysis in smooth conjunction with functional verification, versatile formalisms capturing data, discrete time, and probabilistic aspects are required.

The CONVECS project-team of Inria develops software tools and techniques based on formal methods for the design and verification of asynchronous concurrent systems, which are packaged in the internationally renowned CADP (Construction and Analysis of Distributed Processes) software toolbox. CADP already provides some forms of quantitative analysis for concurrent systems, based upon extended Markovian models and their steady-state or transient analysis. The goals of this post-doctoral fellowship are (a) to propose new formalisms and techniques for the description of properties involving data, discrete time, and probabilities; (b) to devise associated analysis techniques that integrate smoothly with the models and libraries available in CADP; (c) to apply these new formalisms and techniques for the quantitative analysis of an industrial case-study.

This post-doctoral fellowship will be part of the SENSATION European project (2012-2015), funded within the FP7 programme. The work will be carried out in interaction with Saarland University (Saarbrücken, Germany).

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

• Study the state-of-the-art temporal logic-based formalisms suitable for expressing probabilistic properties

• Propose new formalisms for expressing quantitative properties of systems taking into account data, discrete time, and probabilities

• Devise new analysis techniques for these formalisms that combine smoothly with existing CADP libraries

• Model formally an industrial case-study proposed within the SENSATION project using the input languages of CADP (LNT, EXP, etc.)

• Experiment the newly developed analysis techniques on the case-study, and fine-tune the performance of verification

Required skills and profile:

• Good knowledge of formal methods, in particular description languages for concurrent systems (process algebraic languages), quantitative aspects are a plus

• Knowledge of temporal logics and explicit-state verification techniques

• Programming skills, development experience is a plus

• PhD in Computer Science

• Good command of English, French is a plus

• Proven communication and interpersonal relationships skills, attention to detail, methodical approach, autonomy, team player

Contacts:

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

M. Radu Mateescu Inria Grenoble - Rhône-Alpes / CONVECS Inovallée 655, avenue de l'Europe 38330 Montbonnot Saint-Martin Tel : +33 (0)4 76 61 54 86 E-mail : Radu.Mateescu@inria.fr

Application content:

• Letter of application

• Curriculum vitæ including the list of publications

• References or letters of recommendation, if any

Application submission:

Applications should be addressed directly to Radu Mateescu, preferably by e-mail, mentioning the position number #2014A. Applications received after May 31st, 2014 might not be considered if a candidate has been selected already.