Projects

• 2009-2011: French coordinator of the French-Chinese ANR-NSFC project SIVES aiming at developing a SImulation and Verification plateform for developping Embedded Systems.

• 2007-2008: Coordinator of the INRIA ARC project Quotient.

• 2007-2008: French-German cooperation project with Andreas Abel on size-based termination granted by the Bayerisch-Französisches Hochschulzentrum.

• 2006: Young researcher grant from the Conseil Régional de Lorraine on the certification of the termination of computer programs.

• 2003-2006: Member of the ACISI project Modulogic on the design of a platform for building certified software.

• 2002-2005: Member of the RNTL project Averroes on Analysis and VErification for the Reliability Of Embedded Systems.

  Lot 5: technologie de vérification
  Sous-lot 1: ajouter la récriture au noyau de calcul de Coq

  • définition de la classe de réécriture à intégrer [ps]
  • proposition d'architecture du moteur de test de conversion [ps]
  • prototype d'extension du système Coq [ps]
    disponible sur l'archive SVN de Coq (tag "recriture")
    CiME version 2003/06/30 modified: my-cime.tar.gz
  • validation du prototype sur des exemples
  • combinaison à des systèmes de vérification automatique de terminaison [ps]

• 1999-2001: Member of the RNRT project Calife on the development of an environment for formal proof and test of algorithms used in telecommunication.

Last updated on 9 November 2011. Come back to main page.