Contract type : Public service fixed-term contract
Level of qualifications required : Graduate degree or equivalent
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 thesis will be co-advised by Jérôme Feret (Antique team, INRIA Paris) and Gregor Gössler (Spades team, INRIA Grenoble).
Within the ANR project "DCore - Causal Debugging for Concurrent Systems" we are looking for a highly motivated PhD student. The first goal of the thesis is to investigate the use of abstractions for the construction of causal explanations. During the last couple of years, several approaches have been proposed to construct, from the execution of a system violating an expected property P, concise explanations why P was violated, and which components or events caused this violation, see e.g. [JRS04,BBD+12,DF+12,FMN15,GLM15,GS15]. However, these approaches either were limited to small systems, or used ad-hoc approximations to make them scale. The goal of the DCore project is to develop and implement causal analysis for a full-fledged programming language, in order to answer questions of the form "what would have been the outcome if component A had satisfied its specification?" or "which component faults were necessary to entail the observed effect?".
We are therefore interested in developing abstractions that "compose well" with causal analyses, and understanding precisely how explanations found on the abstraction relate to explanations on the concrete system. It is worth noting that the presence of abstraction, which inherently comes with some induction and extrapolation processes, completely recasts the issue of reasoning about causality. Causal traces do no longer describe only potential scenarios in the concrete semantics, but also mix some approximation steps coming from the computation of the abstraction itself. Causal explanation is then intertwined with the issue of alarm diagnosis [R05], and not all explanations are replayable counter-examples: they may contain some steps witnessing some lack of accuracy in the analysis. Vice versa, a research question to be addressed is how to define causal analyses that have a well understood behavior under abstraction. The second goal of the thesis is to implement and validate the theoretical developments as part of a causal debugger for a full-fledged programming language, such as Java with actors, or Erlang.
A description of the thesis subject is available at https://team.inria.fr/spades/phd-thesis-abstractions-for-causal-analysis-and-explanations/
[BBD+12] I. Beer, S. Ben-David, H. Chockler, A. Orni, and R.J. Trefler. Explaining counterexamples using causality. FMSD 40(1), pp. 12-40, 2012.
[DF+12] V. Danos, J. Feret, W. Fontana, R. Harmer, J. Hayman, J. Krivine, C. Thompson-Walsh, and G. Winskel: Graphs, Rewriting and Pathway Reconstruction for Rule-Based Models. Proc. FSTTCS 2012, LIPICS 18, 2012.
[FMN15] T. Ferrère, O. Maler, D. Nickovic: Trace Diagnostics Using Temporal Implicants. Proc. ATVA 2015: 241-258, 2015.
[GLM15] G. Gössler and D. Le Métayer: A general framework for blaming in component-based systems. Sci. Comput. Program. 113(3):223-235, 2015.
[GS15] G. Gössler and J.-B. Stefani: Fault Ascription in Concurrent Systems. Proc. TGC'15, LNCS 9533, 2015.
[JRS04] H. Jin, K. Ravi, and F. Somenzi: Fate and free will in error traces. STTT 6(2):102-116, 2004.
[R05] X. Rival. Abstract Dependences for Alarm Diagnosis. Proc. APLAS 2005, LNCS 3780, 347-363, 2005.
Main activities :
- Study existing work on abstract interpretation, fault diagnosis, and causal analysis.
- Propose abstraction techniques and causal analyses for concurrent programs that "compose well", in the sense that the result of causal analysis on an abstraction of the program has a well-understood interpretation for the concrete program.
- Implement the results as part of a causal debugger for a programming language, such as Java with actors, or Erlang.
Additional activities :
- Present the results at conferences and workshops.
- Participate in project meetings.
Candidates should have a good background in formal methods. Good programming skills are also required.
- 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).
- Theme/Domain : Proofs and Verification
- Town/city : Montbonnot
- Inria Center : CRI Grenoble - Rhône-Alpes
- Starting date : 2019-10-01
- Duration of contract : 3 years
- Deadline to apply : 2019-11-30
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.