[TYPES/announce] Job offer / Researcher-Engineer / Inria & LMF, Saclay, France

[Claude Marche]

Hello to all,

A temporary engineer position at Inria is available in the context of
the ``Decysif'' collaborative project. The main topic of work is
the formal verification of Rust programs using the Creusot environment.

Do not hesitate to forward this announce to anybody possibly interested

== The Decysif project ==

Decysif (https://urldefense.com/v3/__https://decysif.fr/__;!!IBzWLUs!TIqDh4ZOQ1tUd0ptVEsoTlIRNrkoEJxv3UPRRz8e7aZX5SlcasNNUF_etG7e35eMXh4Tfa-B7UVWryzxRA1r3ktrFBN5xMH6n5Lozqk$ ) is a collaborative project joining the
Toccata research team at Inria Saclay, the LMF laboratory of
University Paris-Saclay, and the private companies AdaCore, OCamlPro
and TrustInSoft in Paris.  The general objective of Decysif is to
apply formal verification techniques and tools to the development of
software that is critical for safety and security.

While the Decysif project targets programs written in Ada, C, C++ and
Rust, the proposed engineer position is focused on the verification of
Rust programs, and specifically using the Creusot environment
(https://urldefense.com/v3/__https://github.com/xldenis/creusot__;!!IBzWLUs!TIqDh4ZOQ1tUd0ptVEsoTlIRNrkoEJxv3UPRRz8e7aZX5SlcasNNUF_etG7e35eMXh4Tfa-B7UVWryzxRA1r3ktrFBN5xMH6bSuQnaI$ ). In direct collaboration with the
Why3 developers at Toccata and the research engineers at the
industrial partners, the person recruited will have to work on the
maturation of Creusot. Creusot is a prototype coming from a doctoral
thesis and must be improved to be able to be applied to industrial
case studies. The objectives concern, among other things, the
extension of the supported Rust fragment, the need to complete
specifications of Rust libraries, the improvement of the usability of
the graphical user interface, the increase in the rate of proof
automation, to set up methods to help proof (such as the generation of
counterexamples in case of proof failure), to strengthen the
robustness and reproducibility of proofs.

== Expectations from the candidates ==

We seek candidates with as much experience and skills as possible
in several domains including: development using the OCaml language;
development using the Rust language; techniques for evaluation,
compilation and/or transformation of programs; formal methods for
software engineering; formal logics; static analysis of programs;
computer-assisted theorem proving; use of formal proof environments.

We expect some experience in the field of formal methods of software
engineering in a general sense. The typical candidate would be someone
who recently defended a master's thesis or a PhD in a related domain.

The research part of the job is significant, the work is expected
to lead to academic publications.  The development activities include
a participation in the development of Why3, for which we are
interested in candidates with experience in OCaml programming, or
similar functional programming languages, and in the practice of
shared development using git.

Some skills in the use of a formal proof environment will be a plus.

== How to apply

The engineer position should be filled as soon as possible.

The primary site for the position is

https://urldefense.com/v3/__https://recrutement.inria.fr/public/classic/en/offres/2024-07180__;!!IBzWLUs!TIqDh4ZOQ1tUd0ptVEsoTlIRNrkoEJxv3UPRRz8e7aZX5SlcasNNUF_etG7e35eMXh4Tfa-B7UVWryzxRA1r3ktrFBN5xMH6QMwHWhk$ 

where you can apply with a CV and a motivation letter.

Do not hesitate to contact us directly (Claude.Marche at inria.fr,
Jacques-Henri.Jourdan at cnrs.fr) for more information on the position.