Semantics

BRiefcaSE

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](http://www.fondation-stae.net/) concerned with formal methods for system engineering.

Quarteft

Apr 2009 — Nov 2012. Quarteft (_QUAlifiable Real TimE Fiacre Transformations_) is a project funded by [FNRAE](http://www.fnrae.org/), 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.

TraLaLa

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 …

XML schema, tree logic and sheaves automata

XML documents may be roughly described as unranked, ordered trees and it is therefore natural to use tree automata to process or validate them. This idea has already been successfully applied in the context of Document Type …

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 …

On the Dynamics of PB Systems: A Petri Net View

We study dynamical properties of PB systems, a new computational model of biological processes, and propose a compositional encoding of PB systems into Petri nets. Building on this relation, we show that three properties: …

XML Schema, Tree Logic and Sheaves Automata

XML documents, and other forms of semi-structured data, may be roughly described as edge labeled trees; it is therefore natural to use tree automata to reason on them. This idea has already been successfully applied in the context …

Multitrees Automata, Presburger's Constraints and Tree Logics

We describe _multitree automata_ and a related logic on multitrees. Multitrees are extensions of trees with both associative and associative-commutative symbols that may bear arbitrary numbers of sons. An originality of our approach …