Research engineer / Static analysis of OCaml programs

Inria

France

August 16, 2021

Description

2021-03821 - Research engineer / Static analysis of OCaml programs

Contract type : Fixed-term contract

Level of qualifications required : Graduate degree or equivalent

Fonction : Temporary scientific engineer

Level of experience : From 3 to 5 years

About the research centre or Inria department

The Inria Rennes - Bretagne Atlantique Centre is one of Inria's eight centres and has more than thirty research teams. The Inria Center is a major and recognized player in the field of digital sciences. It is at the heart of a rich R&D and innovation ecosystem: highly innovative PMEs, large industrial groups, competitiveness clusters, research and higher education players, laboratories of excellence, technological research institute, etc.

Context

Inria's Celtique research team is looking for a talented research engineer to contribute to the Salto project, that aims at building a static analyser for OCaml programs. The primary target of the analyser is the implementation of the Tezos blockchain, and the overall goal is to provide added trust in the Tezos codebase, by verifying the absence of errors (unhandled exceptions, integer overflows...) early in the development cycle.

Assignment

As research engineer you will be architecturing the analysis tool, in close collaboration with the researchers associated with the project and with the industrial partner Nomadic Labs. You will be in charge of developing the algorithms that implement the abstract domains and analysis engine, that constitute the core of the tool, and will conduct experiments on a large codebase.

Main activities

The goals of this position comprise:

  • Implementing the main analysis engine for a representative subset of the OCaml language, and implementing the related abstract domains
  • Designing and implementing an incremental version of the analyser Integrating the static analysis tool with a framework for continuous integration

  • Conducting experiments to measure the efficiency and the precision of the analyser

  • Skills

    The candidate will hold a Master (or higher) degree in computer science, and will be acquainted with the topic of program analysis. Experience with developing applications in OCaml is highly recommended. Intimate knowledge of the OCaml toolchain is obviously a plus but not a requirement.

    Benefits package
  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours)
  • Possibility of teleworking
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage
  • Remuneration

    Monthly gross salary from 2562 euros according to diploma and experience

    General Information
  • Theme/Domain : Proofs and Verification
  • Town/city : Rennes
  • Inria Center : CRI Rennes - Bretagne Atlantique
  • Starting date : 2021-10-01
  • Duration of contract : 3 years
  • Deadline to apply : 2021-08-16
  • Contacts
  • Inria Team : CELTIQUE
  • Recruiter : Montagu Benoit / benoit.montagu@inria.fr
  • About Inria

    Inria is the French national research institute dedicated to digital science and technology. It employs 2,600 people. Its 200 agile project teams, generally run jointly with academic partners, include more than 3,500 scientists and engineers working to meet the challenges of digital technology, often at the interface with other disciplines. The Institute also employs numerous talents in over forty different professions. 900 research support staff contribute to the preparation and development of scientific and entrepreneurial projects that have a worldwide impact.

    Instruction to apply

    Please submit online : your resume, cover letter and letters of recommendation eventually

    For more information, please contact benoit.montagu@inria.fr

    Defence Security : This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.

    Recruitment Policy : As part of its diversity policy, all Inria positions are accessible to people with disabilities.

    Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.

    Similar Jobs

    Inria

    France Jun 24, 2021

    Add to favorites Read more...

    Temporary scientific engineer / Software engineering / Vision, perception and multimedia interpretation / Graduate degree or equivalent

    About the research centre or Inria department laboratories of excellence, technological research institute, etc. Inria Rennes - Bretagne Atlantique research center, created in 1980, has a Located at the Beaulieu Campus in Rennes, Inria center...