Research Engineer - Static Analysis Of Ocaml Programs H/F

INRIA

Research engineer / Static analysis of OCaml programs
Le descriptif de l'offre ci-dessous est en Anglais
Type de contrat : CDD

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Ingénieur scientifique contractuel

Niveau d'expérience souhaité : De 3 à 5 ans

A propos du centre ou de la direction fonctionnelle

The Inria center at the University of Rennes is one of eight Inria centers 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 ecosystem of R&D and innovation, including highly innovative SMEs, large industrial groups, competitiveness clusters, research and higher education institutions, centers of excellence, and technological research institutes.

Contexte et atouts du poste

Inria's research team is looking for a talented research engineer to contribute to the project, a static analyser for OCaml programs. The Salto analyser is an abstract interpreter that detects in OCaml programs possibly uncaught exceptions, non-satisfied assertions, integer overflows, and undefined behaviours.

As a research engineer in Épicure, you will work in a team of talented students an researchers, who contribute to the state of the art on the topics of program verification, static analysis, programming language semantics, and compiler verification.

This two-year position is funded by a bilateral contract between and .

The starting date of the position can be discussed and adjusted with the candidate.

Mission confiée

As research engineer, you will contribute to the development of the analysis tool, in close collaboration with the researchers associated with the project. 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.

The goal is to improve the Salto analyser on several aspects: support more features of OCaml; increase the precision of the analysis; improve the performance of the analysis; improve the usability of the tool.

Principales activités

Some more specific goals of this position comprise:

- Upgrading the implementation to support the abstract syntax tree of the 5.X versions of OCaml
- Improving the interval analysis to also track congruences
- Enabling the possibility to analyse specific functions, instead of analysing whole programs only
- Conducting experiments to measure the efficiency and the precision of the analyser

Compétences

The candidate will hold a Ph.D. degree in computer science, and will be acquainted with the topic of static program analysis, and abstract interpretation in particular.
Experience with developing applications in OCaml or in another functional language is highly recommended. Intimate knowledge of the OCaml toolchain is obviously a plus but not a requirement.

Avantages

- 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 exceptional leave (sick children, moving home, etc.)
- Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
- Professional equipment available (videoconferencing, loan of computer equipment, etc.)
- Social, cultural and sports events and activities
- Access to vocational training
- Social security coverage