Apr 2013 — Sep 2016. BRiefcaSE is a basic research project that targets methods involved in the specification, validation and verification of safety critical systems. This project was part of the __IFSE__ working group, an animation and reflexion group, financed by the [RTRA STAE]( concerned with formal methods for system engineering.


Apr 2009 — Nov 2012. Quarteft (_QUAlifiable Real TimE Fiacre Transformations_) is a project funded by [FNRAE](, the Fondation de la Recherche pour l'Aéronautique et l'Espace. The goal of the project is to study formal specification language and qualifiable model transformations in the context of critical embedded systems.


Nov 2004 — Feb 2008. TraLaLA, XML Transformation Languages: logic and applications, is a project funded by ACI MASSES DE DONNÉES. The objectives of the project is to study the processing, querying and manipulation of _data-masses_ (large amounts of data) available in XML format.

A Concurrent Calculus with Atomic Transactions

The _Software Transactional Memory_ (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way …

A Typed Calculus for Querying Distributed XML Documents

We study the problems related to querying large, distributed XML documents. Our proposal takes the form of a new process calculus in which XML data are processes that can be queried by means of concurrent pattern-matching …