[TYPES/announce] Open Engineer Position in ProofInUse joint laboratory

[Claude Marché]

   [Feel free to redistribute this announcement/Apologizes for multiple 
copies]

The Joint Laboratory ProofInUse (https://www.adacore.com/proofinuse) 
hires an experienced R&D engineer (M/F) in the domain of Formal Methods 
for Software Engineering:

      https://jobs.inria.fr/public/classic/en/offres/2018-01034

ProofInUse originates from the sharing of resources and knowledge 
between the Toccata research team (http://toccata.lri.fr/), specializing 
in techniques for deductive program verification and the SME AdaCore, a 
software publisher, specializing in providing software development tools 
for critical systems. The SME TrustInSoft (https://trust-in-soft.com/), 
specialized in advanced static analysis techniques for safety and 
security of C/C++ source code, recently joined the ProofInUse Laboratory.

The purpose of ProofInUse is to increase significantly the number of 
customers of the SPARK 2014 and the TrustInSoft Analyzer technologies, 
by popularizing the use of formal proof techniques. This popularization 
requires the resolution of several scientific and technological 
challenges. A first axis of work is to design and implement a new 
plug-in for deductive verification in the TrustInSoft Analyzer, making 
use of the Why3 intermediate (https://why3.lri.fr/) tool for 
verification condition generation, along the guidelines and design 
choices previously adopted for SPARK, that include strong restrictions 
on the analyzed code regarding the possibility of aliasing in data 
structures. This new plug-in must support new techniques for analyzing 
bit-level and floating-point codes, as well as new facilities for 
providing counterexamples when proofs fail. A second axis of work is to 
leverage the former non-aliasing restrictions, via an alias analysis 
based on a Rust-style sharing control and borrowing. A third axis is to 
actively participate to the development of a formally proved C/C++ 
software library.

The recruited engineer will work in close collaboration with the 
ProofInUse Research and Development team, to address both the scientific 
and the technological challenges presented above. It is expected that 
the engineer contributes both to advancing the academic knowledge in 
ProofInUse context and to the transfer of this knowledge into the 
software products distributed by AdaCore and TrustInSoft. The engineer 
will participate actively to the production of scientific publications, 
and to the software development of the Why3 tool and the TrustInSoft 
Analyzer.

We expect from the candidate some experience with Formal Methods for 
Software Engineering in a broad sense, typically the candidate should 
have defended a PhD in the domain of Formal Methods. More specifically, 
a plus would be some experience in formal logic and proof techniques, in 
automated deduction, in Satisfiability Modulo Theory solvers, in Model 
Checking or in Abstract Interpretation techniques.

The candidate should have a fair experience in software development, a 
plus would be the knowledge of functional programming, and the knowledge 
of the programming languages OCaml, C/C++ and/or Rust.

The candidate should be able to write and speak in English fluently.

The job will take place both on Toccata's lab site in building 650 of 
University Paris-Sud in Orsay, and at TrustInSoft's site in Paris, France.

The position is to be filled as soon as possible starting from Nov 1st 
2018, for a duration of 36 months.

Apply by sending a CV and a motivation letter to the e-mail contact 
addresses below, and/or via the URL given at the top of this message.

Contact/Information: Claude.Marche at inria.fr, 
Benjamin.Monate at trustinsoft.com, Yannick.Moy at adacore.com