Within the French 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. [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.
Candidates should have a good background in formal methods.
Good programming skills are required.
The PhD thesis will be co-advised by Jérôme Feret (Antique team,
INRIA Paris, https://team.inria.fr/antique) and Gregor Goessler
(Spades team, INRIA Grenoble, https://team.inria.fr/spades).
Please do not hesitate to contact us for more information
(firstname.lastname@inria.fr). The starting date is flexible.
To apply online please visit
https://jobs.inria.fr/public/classic/fr/offres/2019-01331
References:
[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.
[R05] X. Rival. Abstract Dependences for Alarm Diagnosis. Proc. APLAS
2005, LNCS 3780, 347-363, 2005.
