I am mainly interested in formal verification of distributed systems. Such systems, that are present in an increasing number of domains, also have more and more critical functions. Formal verification aims at guaranteeing reliability of such systems, i.e. that they match their specification and are bug-free.
The main obstacle towards this end is the growing complexity of distributed systems, illustrated by the so-called combinatorial explosion of the number of behaviours. Several methods are proposed to tackle this combinatorial explosion. During my PhD, my research has mainly been focused on two of them: decision diagrams and the use of symmetries.
Another important challenge of verification is the formal tools used to express the specification of the systems. Several languages exist, most of them being logics such as linear time or computation tree logics. They allow to express qualitative properties, with a yes/no answer. I have recently gained interest in the use of quantitative logics for verification, to express properties whose answer is a numerical value rather than a boolean value.