Research Engineer (M/F) – Scenario-based formal proofs for concurrent software
New
- IT in FTC
- 7 months
- BAC+5
This offer is available in English version
This offer is open to people with a document recognizing their status as a disabled worker.
Offer at a glance
The Unit
Laboratoire d'Informatique de l'Ecole Polytechnique
Contract Type
IT in FTC
Working hHours
Full Time
Workplace
91120 PALAISEAU
Contract Duration
7 months
Date of Hire
01/01/2027
Remuneration
between €3,237 and €3,505 gross per month, depending on experience
Apply Application Deadline : 31 October 2026 23:59
Job Description
Missions
Developing new algorithms for the formal verification of concurrent or distributed systems. Currently, verification algorithms often rely on the user providing complex and frequently unintuitive invariants. Designers of concurrent or distributed systems often provide more operational arguments for the correctness of their implementations—focusing on descriptions of key interleaving scenarios that nonetheless generalize to an unlimited number of threads. In this project, we aim to bridge this gap by elevating scenario-based reasoning—moving from intuitive arguments to formally rigorous ones that are accessible to programmers and can even be automatically derived from source code.
Activity
The main technical components of this work are as follows:
- Formalizing scenarios as what we term the "program execution quotient," which captures a small set of representative interleaved executions that nonetheless generalize—via commutativity—to the set of all executions, even with an unbounded number of threads and an infinite state space.
- Designing languages to represent quotients abstractly in a compact and understandable manner.
- Systematizing the proof process to demonstrate that such an abstraction covers all possible program executions, using novel induction schemes combined with reasoning about commutativity.
- Designing program analysis algorithms to automatically derive quotient abstractions directly from source code.
Your Profil
Skills
The candidate must hold a Master 2 in computer science, with high expertise in theoretical computer science, formal methods, concurrent or distributed systems.
Your Work Environment
The candidate will join the Cosynus formal methods team at LIX (the Computer Science Laboratory at École Polytechnique). LIX is a joint research unit (UMR 7161) affiliated with the CNRS and École Polytechnique. Its research activities span a wide spectrum of fundamental and applied computer science, characterized by a strong interdisciplinary approach. Areas of cutting-edge research include algorithms and complexity, mathematical optimization, artificial intelligence and machine learning, bioinformatics, and systems and networks. LIX benefits from numerous industrial collaborations, particularly with leading companies in the technology, finance, and energy sectors.
Compensation and benefits
Compensation
between €3,237 and €3,505 gross per month, depending on experience
Annual leave and RTT
44 jours
Remote Working practice and compensation
Pratique et indemnisation du TT
Transport
Prise en charge à 75% du coût et forfait mobilité durable jusqu’à 300€
About the offer
| Offer reference | UMR7161-CONENE-003 |
|---|---|
| Line of business | IT, Statistics and Scientific Calculation |
| Job Type | Software Engineering Project Manager or Expert |
| Relevant experience | 1 to 4 years |
About the CNRS
The CNRS is a major player in fundamental research on a global scale. The CNRS is the only French organization active in all scientific fields. Its unique position as a multi-specialist allows it to bring together different disciplines to address the most important challenges of the contemporary world, in connection with the actors of change.
Create your alert
Don't miss any opportunity to find the job that's right for you. Register for free and receive new vacancies directly in your mailbox.