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

[Claude Marche]

Temporary engineer positions at Inria are available for the
``ProofInUse'' consortium.

Do not hesitate to forward this announce to anybody possibly interested

== ProofInUse in short ==

The ProofInUse consortium is a laboratory for research and development
in the domain of high-assurance software. It is joint between several
academic and industrial partners. The general objective of ProofInUse
is to provide software verification tools, based on mathematical
proof, to industry users.

The objective of ProofInUse is to significantly increase the
capabilities and performances of verification environments proposed or
internally used by the partners. Beyond a common interest in formal
verification techniques, the members of ProofInUse share a common
interest in the generic environment Why3 for deductive program
verification, developed in the Toccata research group. In particular,
ProofInUse aims at integration of verification techniques at the
state-of-the-art of academic research, via the Why3 environment.

See also https://urldefense.com/v3/__https://proofinuse.gitlabpages.inria.fr/__;!!IBzWLUs!QMc_4rlyHFEmCJYwwlsDYVlfPVhAWsLtYoIcgA1ePgCHf123jkSgdK47WqFS7Upo507nHGvntYfHI5duZG3oC5SGvnqM3NXf04EhnB4$ 

== Expectations from the candidates ==

We seek for candidates with as much experience and skills as possible
in several domains among : development using the OCaml 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; knowledge of programming languages Ada,
C, C++ and Rust.

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 being expected
to lead to academic publications, as exemplified by the publications
of the former engineers of ProofInUse (see
https://urldefense.com/v3/__https://proofinuse.gitlabpages.inria.fr/dissemination.html__;!!IBzWLUs!QMc_4rlyHFEmCJYwwlsDYVlfPVhAWsLtYoIcgA1ePgCHf123jkSgdK47WqFS7Upo507nHGvntYfHI5duZG3oC5SGvnqM3NXf79KD5qw$ ).  The
development activities include a participation to 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 positions should be filled as soon as possible.

The primary site for the positions is

https://urldefense.com/v3/__https://recrutement.inria.fr/public/classic/fr/offres/2023-05728__;!!IBzWLUs!QMc_4rlyHFEmCJYwwlsDYVlfPVhAWsLtYoIcgA1ePgCHf123jkSgdK47WqFS7Upo507nHGvntYfHI5duZG3oC5SGvnqM3NXfSCLmIX0$ 

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

Do not hesitate to contact me directly (Claude.Marche at inria.fr) for
more information on the positions.