Job offer

Research Field Computer science

Education Level Master Degree or equivalent

Research Field Mathematics

Education Level Master Degree or equivalent

Languages FRENCH

Level Basic

Research Field Computer science

Years of Research Experience 1 - 4

Research Field Mathematics » Algorithms

Years of Research Experience 1 - 4, The candidate must hold a Master in computer science, with expertise in theoretical computer science, formal methods, or concurrent or distributed systems.

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.