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.
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.
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.
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
- 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).
- Theme/Domain :
Embedded and Real-time Systems
Software engineering (BAP E)
- Town/city : Montbonnot
- Inria Center : CRI Grenoble - Rhône-Alpes
- Starting date : 2019-09-01
- Duration of contract : 3 years
- Deadline to apply : 2019-12-31
The keys to success
A Master level education in computer science is required.
A good background (master level) in programming, programming language semantics, programming language implementation (compilation, virtual machines, run-times), and concurency theory (process calculi, bisimulation theory) is required.
A working knowledge of a modern high level programming language such as Ocaml, Python, Java, Scala, or Erlang is required.
A good working knowledge of concurrent / distributed programming is a plus.
A good knowledge of English is required
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.