Job opportunities

Centres Inria associés

Inria Centre at Rennes University

Type de contrat

CDD/Fixed-term contract

Contexte

<p>Inria's&nbsp;<a title="&Eacute;picure research team" href="https://team.inria.fr/epicure/">&Eacute;picure</a> research team is looking for a talented research engineer to contribute to the&nbsp;<a title="Salto static analyser" href="https://salto.gitlabpages.inria.fr/">Salto</a> 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.</p>
<p>As a research engineer in &Eacute;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.</p>
<p>This two-year position is funded by a bilateral contract between&nbsp;<a title="Lexifi" href="https://www.lexifi.com/">Lexifi</a> and <a title="Inria" href="https://www.inria.fr/">Inria</a>.</p>
<p>The starting date of the position can be discussed and adjusted with the candidate.</p>

Mission confié

<p>As research engineer, you will contribute to the development of the&nbsp;<a title="Salto" href="https://salto.gitlabpages.inria.fr/">Salto</a> 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.</p>
<p>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.</p>

Principales activités

<p>Some more specific goals of this position comprise:</p>
<ul>
<li>Upgrading the implementation to support the abstract syntax tree of the 5.X versions of OCaml</li>
<li>Improving the interval analysis to also track congruences</li>
<li>Enabling the possibility to analyse specific functions, instead of analysing whole programs only</li>
<li>Conducting experiments to measure the efficiency and the precision of the analyser</li>
</ul>

Compétences

<p>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.<br /> 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.</p>

Référence

2026-09842

Thème

Proofs and Verification

Domaine d'activité

Software engineering

Research engineer / Static analysis of OCaml programs

Job opportunities

Centres Inria associés

Inria Centre at Rennes University

Type de contrat

CDD/Fixed-term contract

Contexte

<p>Inria's&nbsp;<a title="&Eacute;picure research team" href="https://team.inria.fr/epicure/">&Eacute;picure</a> research team is looking for a talented research engineer to contribute to the&nbsp;<a title="Salto static analyser" href="https://salto.gitlabpages.inria.fr/">Salto</a> 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.</p>
<p>As a research engineer in &Eacute;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.</p>
<p>This two-year position is funded by a bilateral contract between&nbsp;<a title="Lexifi" href="https://www.lexifi.com/">Lexifi</a> and <a title="Inria" href="https://www.inria.fr/">Inria</a>.</p>
<p>The starting date of the position can be discussed and adjusted with the candidate.</p>

Mission confié

<p>As research engineer, you will contribute to the development of the&nbsp;<a title="Salto" href="https://salto.gitlabpages.inria.fr/">Salto</a> 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.</p>
<p>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.</p>

Principales activités

<p>Some more specific goals of this position comprise:</p>
<ul>
<li>Upgrading the implementation to support the abstract syntax tree of the 5.X versions of OCaml</li>
<li>Improving the interval analysis to also track congruences</li>
<li>Enabling the possibility to analyse specific functions, instead of analysing whole programs only</li>
<li>Conducting experiments to measure the efficiency and the precision of the analyser</li>
</ul>

Compétences

<p>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.<br /> 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.</p>

Référence

2026-09842

Thème

Proofs and Verification

Domaine d'activité

Software engineering