We have recently started a Joint Laboratory between the French INRIA research labs and AdaCore, to further develop the Why3 and SPARK technologies used inside the SPARK 2014 tools. You'll find a high level description of our goals here:
http://www.spark-2014.org/proofinuse We are now looking for two R&D engineers to complete the team of researchers (INRIA) and engineers (AdaCore). It is expected that the engineers contribute both to advancing the academic knowledge in ProofInUse context and to the transfer of this knowledge into the software products distributed by AdaCore. Concretely, the engineer will participate actively to the production of scientific publications, to the software development of SPARK-related tools, and to the support for AdaCore customers. 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 and Ada. The candidate should be able to write and speak in English fluently. For all details and contacts, see the description of the position at INRIA: http://www.inria.fr/en/institute/recruitment/offers/r-d-engineers/%28view%29/details.html?id=PNGFK026203F3VBQB6G68LOE1&LOV5=4510&ContractType=6502&LG=EN&Resultsperpage=20&nPostingID=8315&nPostingTargetID=14052&option=52&sort=DESC&nDepartmentID=10 -- Yannick Moy, Senior Software Engineer, AdaCore _______________________________________________ Why3-club mailing list Why3-club@lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/why3-club
