Research & teaching activities

Research

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.

Publications

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

Realisation

You can find all files from my thesis at gforge.inria.fr

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

Teaching

All teaching activities are given at ENSEM.

2006-2007

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.

2007-2008