Researcher (M/F) - Scenario-based formal proofs for concurrent software
New
- Researcher in FTC
- 8 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
Researcher in FTC
Working hHours
Full Time
Workplace
91120 PALAISEAU
Contract Duration
8 months
Date of Hire
01/12/2026
Remuneration
Between €3,237.95 and €3,505.53 gross, depending on experience.
Apply Application Deadline : 22 August 2026 23:59
Job Description
Missions
The primary objective of this position is to develop new algorithms for the formal verification of concurrent or distributed systems.
Activity
Modern software increasingly employs concurrent programming to leverage the performance benefits of multi-core architectures. In particular, deep learning model training is often parallelized to handle the massive increase in parameter counts. However, concurrent programming is notoriously difficult, and concurrency bugs occur even in code written by the most experienced programmers. Consequently, researchers have developed mathematical reasoning techniques, hoping that formal proofs could solve this problem. Unfortunately, many logic-based proof techniques—such as rely-guarantee, Owicki-Gries, and others—rely on the user to provide complex and often counter-intuitive invariants. In contrast, algorithm designers in the distributed computing community frequently provide more operational arguments for the correctness of their implementations; these focus on descriptions of key interleaving scenarios yet generalize to an arbitrary number of threads. In this project, we aim to bridge this gap and elevate scenario-based reasoning from intuitive arguments to formally rigorous ones that are accessible to programmers and can even be automatically derived from source code. The goal is to develop fundamental techniques, algorithms, and automated tools demonstrating that scenario-based reasoning can be both rigorous and accessible to everyday programmers. We will formalize scenarios as what we term the "execution quotient" of a program; this captures a small set of representative interleaved executions that—via commutativity—generalize to the set of all possible executions, even with an arbitrary number of threads and an infinite state space. We will demonstrate that these quotients can be described succinctly in a suitable language and that it is possible to derive them automatically directly from the source code. ...and that programmers can use these derivations and query them to better understand the concurrent behaviors of their implementations. The main components of this project will be:
- Establishing formal foundations for execution quotients to enable scenario-based reasoning.
- Designing languages to represent quotients abstractly in a compact and understandable way.
- Systematizing the proof process to demonstrate that such an abstraction covers all possible program executions, using new 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 in computer science, with expertise in theoretical computer science, formal methods, or 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.95 and €3,505.53 gross, 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-001 |
|---|---|
| CN Section(s) / Research Area | Information sciences: bases of information technology, calculations, algorithms, representations, uses |
| 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.