This offer is obsolete and is retained for reference only. Current offers are available on this page.
Implementation and formal proof of a compression service based on the Deflate algorithm
As a Research & Development Engineer, you will join a team in charge of creating models (both high-level and implementation-level) of sensitive software components using Prove & Run’s tools.
More specifically, you’ll be in charge of creating the implementation and formal proof of a compression service based on the Deflate algorithm used by many compressed file formats (.zip, .gz, .png, etc). In particular, you will work on the correctness of the compression/decompression algorithm and the compliance of the compressed data stream generated by your tool with the standard defined by RFC1951. Not only will you develop a formally correct compression service, but it will be fully compliant with other existing tools. More details are available in this presentation.
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
- Automated Deduction and/or Interactive Proving
- Algorithms / Data Structures
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).