## About me

I am currently a postdoctoral researcher at Université Sorbonne Paris Nord, LIPN (Villetaneuse) in LoVe team, affiliated to the ANR project
BisoUS .
I'm working on opacity for parametric timed automata.

I did a Ph.D. in Computer Science
on verification of distributed systems
in Université Côte d'Azur, under the supervision of
Pr. Etienne Lozes
and
Dr. Cinzia Di Giusto
.

My main interests are modelling and formal methods.

Download my CV here

### Ph.D. Subject

#### Title: Synchronizability for distributed systems

Download my thesis here

A very short explanation: Participation to "Ma thèse en 180 secondes"
**Abstract**

**Distributed systems** are ubiquitous and their implementation is complex and error-prone.
In order to check for errors, they can be modeled as systems of **communicating automata**,
where each automaton represents the behavior of an element of the system. Verification
problems such as reachability are undecidable in such a model. Indeed, a system of
communicating automata is Turing-equivalent. For that, the use of approximations is
necessary. **k-synchronizability** is one of these techniques. A system is k-synchronizable if,
for all executions, there is an equivalent execution that can be divided into phases
containing k messages. These phases are called k-exchanges. In this thesis, we analyse
k-synchronizable systems: we show that reachability is decidable and we are interested
in the membership problem, that is: given a system, decide whether it is k-synchronizable.
We study both the case where k is an input of the problem, and the case where we have to
guess a k such that the system is k-synchronizable. We study them according to the **type
of communication** of the system. Either the system is in mailbox and so each process
has only one buffer to store all received messages, or the system is in peer-to-peer,
and each process has a buffer for each sender. Both problems are decidable when the system
is communicating in mailbox. When the system is communicating in peer-to-peer, the first one
is decidable and the second remains open. Finally, we point out some counter-intuitive cases
of k-synchronizable systems that lead us to propose some variations to the definition of
k-synchronizability. A comparative study of the state-of-art classes of systems and our new
classes concludes our work.