Researcher (M/F) - Scenario-based formal proofs for concurrent software

Organisation/Company CNRS Department Laboratoire d'Informatique de l'Ecole Polytechnique Research Field Computer science Mathematics » Algorithms Researcher Profile Recognised Researcher (R2) Application Deadline 22 Aug 2026 - 23:59 (UTC) Country France Type of Contract Temporary Job Status Full-time Hours Per Week 35 Offer Starting Date 1 Dec 2026 Is the job funded through the EU Research Framework Programme? Not funded by a EU programme Is the Job related to staff position within a Research Infrastructure? No

Offer Description

The primary objective of this position is to develop new algorithms for the formal verification of concurrent or distributed systems.

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.

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.

The candidate must hold a Master in computer science, with expertise in theoretical computer science, formal methods, or concurrent or distributed systems.