The Coq mailing list

[Claude Marche <Claude.Marche AT inria.fr>]

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

== 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://proofinuse.gitlabpages.inria.fr/

== Expectations from the candidates ==

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 PhD in a related domain. Having a PhD
is not a mandatory requirement though.

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://proofinuse.gitlabpages.inria.fr/dissemination.html).  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://recrutement.inria.fr/public/classic/en/offres/2021-04144

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.