return

Job details

Job posted by AdaCore (03/04/2014 09.49)

Engineer R&D in Formal Methods for Software Engineering

  !   Offer by Large Company/SME

Please note that the job is no longer active!

The Joint Laboratory ProofInUse originates from the sharing of resources and knowledge between the Toccata research team, specializing in techniques for program proofs and the SME AdaCore, a software publisher, specializing in providing software development tools for critical systems.

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.

We expect from the candidate some experience with Formal Methods for Software Engineering, 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.

Description

About Inria and the job

Established in 1967, Inria is the only French public research body fully dedicated to computational sciences.

The job is directly funded by the Joint Laboratory « ProofInUse » (http://www.spark-2014.org/proofinuse). The objective of ProofInUse is to provide verification tools, based on mathematical proof, to industry users. These tools would be aimed at replacing or complementing the existing test activities, whilst reducing costs. ProofInUse originates from the sharing of resources and knowledge between the Inria team « Toccata » (http://toccata.lri.f)) specializing in techniques for program proofs and the SME « AdaCore » (http://www.adacore.com), a software publisher, specializing in providing software development tools for critical software technology. A previous successful collaboration between Toccata and AdaCore enabled Toccata’s Why3 technology, to be put into the heart of the AdaCore-developed SPARK technology.

Mission

The purpose of ProofInUse is to increase significantly the number of industrial customers of the SPARK technology, thus democratizing the use of proof techniques.

This democratization requires the resolution of several scientific and technological challenges. A first axis of research and innovation is to facilitate the use of automatic provers. A second axis of research and innovation is to allow the user to go beyond what is possible with the current SPARK technology, in terms of specification of programs and the proofs of these specifications.

Job offer description

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.

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.

Skills and profile

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.

Nr of positions available : 2

Research Fields

Computer science - Programming

Career Stage

Experienced researcher or 4-10 yrs (Post-Doc)

Research Profile

First Stage Researcher (R1)

Benefits

Canteen and cafeteria
Sports equipment
Local transport reimboursment
35 vacation days per year

Comment/web site for additional job details

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

http://www.spark-2014.org/proofinuse




Requirements

Required Research Experiences
Main Research Field Computer science
Research Sub Field Programming
Required Languages
Language ENGLISH
Language Level Good
Required Education Level
Degree Field Computer science
Required Research Experiences
Years of Research Experience 4
Required Education Level
Degree PhD or equivalent
GET MORE! The EURAXESS Services Centres
 

To better plan and organise their stay in a foreign European country, researchers and their families can also benefit of the free and personalised assistance offered by the EURAXESS Services Centres, a network of more than 200 centres located in 40 different European countries.

Application Deadline

01/10/2014

Envisaged Job Starting Date

01/10/2014

Application e-mail

moy@adacore.com

Other job details
Job ID

33914564

Country

FRANCE

Type of Contract

To be defined

Status

Full-time

Street

46 rue d'Amsterdam

Hours Per Week

40

City

Paris

Postal Code

75009

Company/Institute

AdaCore

EU Research Framework Programme
Is the job funded through the EU Research Framework Programme?

No

Company/Institute
AdaCore

Small Medium Enterprise
46 rue d'Amsterdam
75009 - Paris
FRANCE
email moy@adacore.comhttp://www.adacore.com

QR-Code