[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.mar...@inria.fr,
benjamin.mon...@trustinsoft.com, yannick....@adacore.com
_______________________________________________
Why3-club mailing list
Why3-club@lists.gforge.inria.fr
https://lists.gforge.inria.fr/mailman/listinfo/why3-club
