Jobs
Researcher in Formal Methods (M/F)
Posted on the 25th January 2024
- Permanent position
Location: Rennes (35), France
Website: http://www.fr.mitsubishielectric-rce.eu/
Job Reference: INSPE025
Contract: permanent from April 1st, 2024
Context and description
As a subsidiary of the Mitsubishi Electric Group, a global leader in electrical and electronic products and systems, MITSUBISHI ELECTRIC R&D CENTRE EUROPE includes a division named “Communication and Information Systems” (CIS). This division specializes in communication and control solutions for applications targeting both professional and consumer-oriented sectors. Specifically, the CIS division engages in research activities encompassing multi-approach Formal Methods (such as Deductive Verification, Abstract Interpretation, proof assistants, etc.) across various domains, including automotive, railway, factory automation, robotics, aerospace, nuclear, and hardware and software development.
Located in Rennes (Ille-et-Vilaine, Brittany), the CIS division is seeking a researcher with expertise in Formal Methods to undertake the following responsibilities:
. Research on innovative solutions for critical and non-critical systems, with a focus on security, safety, or business activities using Formal Methods;
. Study and develop prototypes of software tools and engineering methodologies to facilitate the application of Formal Methods in an industrial context, spanning from proof of concept to pre-production tools;
. Clearly demonstrate the effectiveness of proposed solutions to both technical and non-technical stakeholders;
. Contribute to open innovation in the field of Formal Methods by collaborating with academic partners through joint research projects, co-supervision of doctoral students, direct contracts, etc.
Required education and experience
The ideal applicant has:
. At least 3 years’ experience (including a Ph.D. in the field of Formal Methods) in software and hardware development or mathematics, gained within public or private R&D laboratories;
. Experience in Formal Methods and possibly in one or more of the following areas: automotive, railway, industrial automation, model engineering, control theory, software engineering, FPGA and similar hardware developments, testing, industrial and optical networks, Artificial Intelligence (Deep & Machine Learning, Genetic Algorithms, etc.); • Applied knowledge and expertise related to one or more Formal Methods tools (such as Atelier B, Frama-C, SPARK, SCADE, Why3, Boogie, Agda, Coq, Lean, Isabelle, TrustinSoft Analyzer, PolySpace, Astrée, Z3, CVC5, Alt-Ergo, SPIN, NuSMV, Simulink Design Verifier, UPPAAL, etc.);
. Established research experience evidenced by publications or patents;
. A strong knowledge of functional (OCaml, Haskell, etc.), object-oriented (C++, C#, Java, etc.), or synchronous languages (SCADE, Lustre, etc.), as well as software engineering practices, will also be highly appreciated.
Personal profile
. Open-mindedness, capacity to work in a multicultural and international environment;
. Ability to work across multiple tasks methodically and efficiently, within set deadlines;
. Motivation to work in a dynamic industrial research environment and adaptability in reordering priorities;
. Excellent communication and interpersonal skills: ability to share information with team players (must show evidence of teamwork), and to present one’s work to a wide audience (demonstrators, presentations, etc.) in an understandable and appealing fashion;
. Fluent written and spoken English;
. Availability for business trips abroad.
Contact
Magali BRANCHEREAU (Human Resources Manager)
Please send your C.V. and cover letter in English as PDF files to jobs@fr.merce.mee.com
specifying your name followed by the reference of the job posting INSPE025 in the subject line.
Download the PDF version