2017-00011 - Formal methods and verification of hardware circuits

Contract type : Public service fixed-term contract

Renewable contract : Oui

Level of qualifications required : Graduate degree or equivalent

Other valued qualifications : MSc or PhD in computer science

Fonction : Temporary scientific engineer

About Inria

Inria, the French National Institute for computer science and applied mathematics, promotes “scientific excellence for technology transfer and society”. Graduates from the world’s top universities, Inria's 2,700 employees rise to the challenges of digital sciences. With its open, agile model, Inria is able to explore original approaches with its partners in industry and academia and provide an efficient response to the multidisciplinary and application challenges of the digital transformation. Inria is the source of many innovations that add value and create jobs.

About the research centre or Inria department

The Inria research center of Grenoble - Rhône Alpes gathers nearly 730 workers organized in 34 research teams and 9 services that support research


The proposed job is part of the French research project Securiot-2 that aims at developing novel methods to enable the design and certification of circuits for the Internet of Things.

The objective is to improve the CADP verification toolbox (http://cadp.inria.fr) developed by the CONVECS team and to apply this toolbox to verify whether a circuit is robust with respect to faults.




Assignments :
With the help of researchers from the CONVECS team, the recruited person will be taken to develop various improvements of the CADP tools, as well as specify and analyze hardware circuits formally.

For a better knowledge of the proposed research subject :
Scientific references are available at the following URL, do not hesitate to log in: http://convecs.inria.fr

Collaboration :
The recruited person will work with the researchers of the CONVECS team and also with the parteners of the Securiot-2 project, in particular the Tiempo company.

Main activities

The planned activities will consist, on the one hand, in participating to the formal description of the examples of circuits under scrutiny, in modelling various faults (either transient or permanent) at the logical-gate level, and to study the impact of such faults on the circuit behaviour, and, on the other hand, in contributing to enhancements of the CADP software tools according to the needs that will arise during the project.



Knowledge about formal methods, and/or skills in C-language programming, and/or competences in hardware circuit design would be an asset.

Languages : English proficiency is desirable

Relational skills : team player, autonomy


Benefits package

  • Subsidised catering service
  • Partially-reimbursed public transport
  • Social security
  • Paid leave
  • Flexible working hours
  • Sports facilities


Gross annual salary to 30700 euros according to experience and diplomas