Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[Frama-c-discuss] Open Engineer Position in ProofInUse joint laboratory
- Subject: [Frama-c-discuss] Open Engineer Position in ProofInUse joint laboratory
- From: Claude.Marche at inria.fr (Claude Marché)
- Date: Wed, 12 Sep 2018 14:43:12 +0200
[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
- Prev by Date: [Frama-c-discuss] Thesis about Frama-C and E-ACSL
- Next by Date: [Frama-c-discuss] JFLA 2019 : second appel à communications
- Previous by thread: [Frama-c-discuss] Thesis about Frama-C and E-ACSL
- Next by thread: [Frama-c-discuss] JFLA 2019 : second appel à communications
- Index(es):