Ph.D. funding available at Univ. Grenoble Alpes / Verimag (France)

h.D. funding available at Univ. Grenoble Alpes / Verimag (France)

Supervisors: Saddek Bensalem and Yliès Falcone, Univ. Grenoble Alpes (emails: 
<> and <>)

This thesis aims at complementing rigorous system design with runtime verification techniques for cyber-physical 
systems (CPSs).

In particular, we are interested in the following important features of CPSs: real-time behavior, distributed 
execution, and architecture dynamicity.

A rigorous system design flow is a formal accountable and iterative process for deriving trustworthy and 
optimized implementations from application software and models of its execution platform and its external 
environment. Rigorous system design is a formally defined process decomposed into steps. It is also model-based: 
successive system descriptions are obtained by the application of correct-by-construction source-to-source of 
a single expressive model rooted in well-defined semantics. An additional demand is accountability that is the 
possibility to explain which among the requirements is satisfied and which may not be satisfied.

Runtime verification (RV) is the umbrella term to encompass all aspects of monitoring and analysis of hardware, 
software and the executions of systems in general. RV techniques are lightweight dynamic techniques to assess 
and enforce correctness, reliability, and robustness during system execution. These techniques are significantly 
more powerful, versatile and rigorous than conventional testing, and more practical than exhaustive formal

The RSD Research Group ( <>) seeks motivated 
candidates with a Masters degree in CS and a solid background on some of the following topics algorithms, 
automata, logic, formal methods, machine learning, and statistical reasoning.

Such candidates who are ready to learn new things and complete their background are kindly requested to send 
an e-mail (with "PhD candidate" in the title) with:
- a CV,
- a motivation letter, and
- recommendation letter(s),
to <> and 

The Grenoble area, in addition to being surrounded skiable mountains is easily accessible: Lyon (1 hour), 
Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train) and Barcelona (6 hours). It features one of 
Europe’s largest concentrations of academic/industrial research and development with a lot of students, 
a cosmopolite atmosphere and work opportunities.

VERIMAG, is a leading academic lab in verification and model-based design of embedded cyber-physical systems. 
Its past contributions include model checking (J. Sifakis, Turing Award 2007), the data-flow language Lustre 
(P. Caspi, N. Halbwachs) underlying the SCADE programming environment for safety-critical systems.

Comments are closed.