Research engineer / Static analysis of OCaml programs

Research engineer / Static analysis of OCaml programs

Level of qualifications required : PhD or equivalent

Fonction : Temporary scientific engineer

Level of experience : From 3 to 5 years

About the research centre or Inria department

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.

Context

Inria'sÉpicure research team is looking for a talented research engineer to contribute to theSalto 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 betweenLexifi and Inria .

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

Assignment

As research engineer, you will contribute to the development of theSalto 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.

Main activities

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

Skills

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.

Benefits package

• 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
• Theme/Domain : Proofs and VerificationSoftware engineering(BAP E)

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.

Instruction to apply

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

Defence Security : This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 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.

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.