Research & teaching activities


I am interested in Lock-free algorithms. I especially want to prove their correctness by using proof-assistant.

At the beginning my project proposal was to apply well-known methods in my research team MOSEL to lock-free algorithms. Those methods are B, TLA+ and model-checking. Those methods imply a top-down approach. So the idea was to develop new algorithms.

Since then I discovered a lot of algorithms and a lot of work on developing such algorithms. But proofs were very rare and none of them were written within a proof-assistant. Therefore, I want to justify lock-free algorithms by applying well-known methods, and in particular B and TLA+.

Note also that my work is supported by Microsoft Research through its European PhD Scholarship Programme.


To keep in touch with my publications, you can subscribe to the RSS Channel of my publications.


You can find all files from my thesis at

While not directly related to my subject, DIXIT is an editor for predicate diagrams I wrote when I was working as a research engineer.


All teaching activities are given at ENSEM.


I gave 21 hours of TP to the first year students. I have also given 7h30 of TD and 27h of TP to the second year one. It is an equivalent of 43h30 of TD.