Current Projects

  • BWare (ANR INS, since 2012, global coordinator). The goal of this project is to build a mechanized and proof-based generic platform for the automated verification of B proof obligations (coming from the modeling of industrial applications in particular). This platform will consist of several verification tools (first order automated theorem provers and SMT solvers).

Former Projects

  • ModuLogic (ACI "Sécurité Informatique", 2003-2007). This project aimed to design a modular and logically founded environment to build software-based systems able to meet high safety requirements. In particular, this environment had to be based on the Focalize system.
  • EDEMOI (ACI "Sécurité Informatique", 2003-2007). The goal of this project was to integrate and apply several requirements engineering and formal methods techniques to analyze regulation standards in the domain of airport security. In particular, these standards were formalized using Focalize, as well as Atelier B.
  • A3PAT (ANR blanc, 2005-2009). The aim of this project was to fulfil the important need for externalization of proofs using rewriting techniques and in a "skeptical" way (i.e. an approach where we do not "believe" the external procedures).
  • CerPAN (ANR blanc, 2005-2009, Cedric/Cnam coordinator). The objective of this project was to develop and apply methods which allow us to formally prove the soundness of programs from numerical analysis.
  • SSURF (ANR SETIN, 2007-2010). This project aimed to develop a formal framework in order to study various security properties (e.g. access control policies, together with their implementations), and to consider an implementation of this formal framework in the Focalize system in particular.
  • Quotient (ARC Inria, 2007-2008). The goal of this project was to study the use of concrete types with invariants. In particular, the Moca tool, which is a generator of construction functions for OCaml data types with invariants, was developed in this project and allows us to ensure invariants over concrete types.
  • ENVIEVERTE (DIM Région Île-de-France/Digiteo, since 2010). The aim of this project is to build a complete model which allows us to refine textual descriptions into formal representations in the framework of the configuration of intelligent environments, and in order to provide reliable and easy to use configuration tools.