[Agda] CIFRE PhD thesis position in Siemens Mobility, Chatillon

[Danko Ilik]

SUBJECT

Optimization of source code for safety-critical systems

SUPERVISORS
    • Thesis supervisors:
        ◦ Danko Ilik at Siemens Mobility
        ◦ Lutz Strassburger at LIX, Ecole Polytechnique

CONTEXT

The research work on the thesis will take place at Siemens Mobility in
Chatillon, France, a division providing the computer systems (hardware
and software) for many on the World's automatic metros.

Being safety-critical, our computer systems are certified according to
the norm EN 50126/50128/50129. To achieve the highest safety integrity
level (SIL4), for some of our components, we use formal methods based
on mathematical proof and programming languages technology. We are one
of the pioneers of using such methods in industry, with our work on
Paris's line 14.

The use of formal methods in large and real-life projects poses
interesting challenges for the optimization of execution time of
software derived using the formal methods.

OBJECTIVES

The goal of the thesis will be to develop ways to optimize the
performance of software, while not sacrificing the guarantees of
safety already provided for non-optimized code.

It is expected that the PhD candidate will implement the methods
discovered, and that a certification according to the relevant safety
norms be prepared for the implementation.

Necessarily going beyond the state-of-the-art, the candidate is
expected to obtain an independent confirmation of the novelty of
her/his results (in form of a scientific publication or patent) and
write a PhD thesis that she/he will defend.

QUALIFICATIONS

The PhD candidate should preferably have a previous training or a
first research experience in 2 of the following 3 areas:

    • programming languages topics, such as functional programming,
compiler construction or semantics of programming languages;

    • proof formalization, i.e., knowledge of proof assistants (Coq,
Agda, Isabelle, etc.);

    • computer architecture, especially topics about out-of-order
execution of modern CPUs (cache behaviour, branch prediction, etc.).

EMPLOYMENT TERMS

The PhD researcher will be engaged under a 3-year work contract
(French CDD) at Siemens Mobility in Chatillon.

The start of the PhD thesis and the work contract may be conditioned
by the fulfillment of the Qualification and ZRR admission procedures
of the doctoral school (Ecole Polytechnique, Palaiseau).

ADMISSION PROCEDURE

The application can be submitted at the Siemens Mobility web site, at
the address:
    https://jobs.siemens-info.com/jobs/66150?lang=en-gb

We encourage candidates to send their application ASAP.