Research & Development Engineer – Internship – RDEI-2014-2 – Obsolete

This offer is obsolete and is retained for reference only. Current offers are available on this page.


Extend our code generation process and use this extension to enable our modeling tools to prove a part of themselves.


As a Research & Development Engineer, you will interact both with the team in charge of developing our Integrated Modeling Environment (IME), and with the team in charge of creating models of sensitive software components using that IME. More precisely, you will:

  • extend the compiler that transforms programs written with our modeling language into C source code,
  • model, with our IME, some of its own proof search algorithms.

Our modeling language is a functional language. This language is compiled to an intermediate imperative language, allowing our tools to generate efficient C code. The first objective of this internship will consist in implementing a new compiler from this intermediate language to Java.

The second objective will be to use this compiler to generate new implementations of two proof search algorithms. These two algorithms are already part of the IME, but their current implementations have been written manually.  These new implementations will be written using our modeling language and will be specified and proved using our IME.

The third objective will be to integrate these generated algorithms back with our IME, which is written in Java. This will require you to complete the compiler implemented during the first part of the internship with linking information. Finally, you will compare the performance of the generated implementations against the original implementations.

This is offer is for a 6-month internship and is located in our office in Paris.


You are currently completing a Master’s Degree or an equivalent degree. You have a significant experience of software development. You are rigorous, independent and have good interpersonal skills.

An interest in one or more of the following topics will be appreciated positively:

  • Program Verification
  • Compilation
  • Interactive Proving
  • Specifying algorithms

Previous experience with the following tools with help ensure that you can hit the ground running:

  • The Eclipse development environment
  • Source code management tools
  • Issue tracking systems

A good level of English is required.


All interns will receive the following benefits:

  • Compensation of €1000-1200/month (gross),
  • Daily meal stipends (Tickets Restaurant),
  • Half of the monthly cost of the Navigo card (the public transportation card in Paris).


Are you interested in joining Prove & Run and becoming a key part of our team? If so, please check what it means to be an intern at Prove & Run, or apply right away!

Print Print