2019-01274 - PhD Position F/M Reversible debugging for concurrent and distributed systems

Contract type : Public service fixed-term contract

Level of qualifications required : Graduate degree or equivalent

Other valued qualifications : Master level eduction

Fonction : PhD Position

About the research centre or Inria department

Inria the French national institute for research in computer science and control, is dedicated to fundamental and applied research in information and communication science and technology (ICST). Inria has a workforce of 3,800 people working throughout its eight research centers established in seven regions of France.

Grenoble is the capital city of the French Alpes. Combining the urban life-style of southern France with a unique mountain setting, it is ideally situated for outdoor activities. The Grenoble area is today an important centre of industry and science (second largest in France). Dedicated to an ambitious policy in the arts, the city is host to numerous cultural institutions. With 60,000 students (including 6,000 foreign students), Grenoble is the third largest student area in France.


The PhD will be funded by the French National research Agency (ANR) project DCore, whose aim is to develop a new debugging technology for concurrent and distributed systems.


Under the guidance of Prof. Ivan Lanese and Jean-Bernard Stefani, the PhD work will take place in the context of the DCore project. DCore aims at developing a new debugging technology for concurrent and distributed systems based on concurrent reversibility and causality analysis. The PhD work will concern more specifically the semantical foundations and the implementation of an experimental reversible debugger for concurrent and distributed actor programs such as e.g. Erlang programs or Java/Scala Akka programs. A reversible debugger allows a programmer to explore a program execution by moving forward and backward in the execution when looking for a bug. While reversible debuggers are well-known for standard sequential programs, this is not the case for concurrent and distributed programs, where going backward in an execution is not as simple as undoing the last executed instructions, but may involve backtracking consistently in different concurrent threads of execution.

In this context, the goal of the PhD is twofold: (1) to study the formal operational semantics aspects of a reversible debugger for concurrent or distributed programs in a state of the art actor language, (2) to develop a proof-of-concept prototype reversible debugger for the chosen actor language, and to assess its benefits and performance.

For a better knowledge of the proposed research subject :
A good starting point for the PhD work will be the reversible debugger for Erlang developed by Lanese et al.:

Ivan Lanese, Naoki Nishida, Adrian Palacios, German Vidal: CauDEr: A Causal-Consistent Reversible Debugger for Erlang, 14th Int. Symp.. Functional and Logic Programming (FLOPS) 2018.

the theory of causal-consistent debugging described in:

Ivan Lanese: From Reversible Semanics to Reversible Debugging, 10th Int. Conf. Reversible Computation (RC) 2018.

and the theory of causal-consistent reversible concurrent languages studied in:

Ivan Lanese, Claudio Antares Mezzina, Jean-Bernard Stefani:
Reversibility in the higher-order π-calculus. Theoretical Computer Science 625, 2016.

Collaboration :
The ANR Dcore project involves the collaboration of the following research teams: the Spades team at INRIA Grenoble, the Focus team at INRIA Sophia and Bologna University, the Antique team at INRIA Paris, and the IRIF laboratory at Paris-Diderot University. The PhD work will be conducted as part of this collaboration.

Responsibilities :
The PhD student recruited will be expected to contribute to the DCore research effort, and to conduct research on the two main objectives of the thesis: semantical foundations for reversible debugging, and proof of concept implementation of a reversible debugger for an actor language.

Main activities

The main activities during the PhD work will comprise:

  • Studying the state of the art on concurrent and distributed debugging, reversible debugging, and reversible concurrent calculi and languages.
  • Studying the formal operational semantics of causal-consistent reversibility in actor languages, taking into account various features such as exception handling, modules, input/output facilities, and the use of external libraries or services.
  • Developing a proof-of-concept prototype of a reversible debugger for a state of the art actor language such as Erlang or Java/Scala with Akka, and assessing its usability, performance, and scalability.


Technical skills required:

  • mathematical and logical skills to conduct proofs and the formal analysis of programs and algorithms
  • programming skills to conduct complex program developements

Soft skills required:

  • scientific curiosity
  • team working
  • presentation skills

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage


Salary: 1982€ gross/month for 1st and 2nd year. 2085€ gross/month for 3rd year.

Monthly salary after taxes : around 1596,05€ for 1st and 2nd year. 1678,99€ for 3rd year. (medical insurance included, income tax excluded).