Grants and contracts

Ongoing grants

  • Verasco (formal verification of static analyzers and compilers), coordinator. ANR-11-INSE-003, 2012-2015.
  • ADN4SE (process and tools to support the rapid development of embedded software with strong safety constraints). Fonds national pour la Société Numérique, BGLE call, 2012-2016.
  • BWare (mechanized framework to support the automated verification of proof obligations coming from the development of industrial applications using the B method and requiring high guarantees of confidence). ANR-12-INSE-0010, 2012-2016).
  • CEEC (certification of a high-assurance execution environment), Fonds national pour la Société Numérique, BGLE call, 2011-2014.
  • Paral-ITP (parallelization of interactive theorem provers). ANR-11-INSE-001, 2011-2014.
  • Tools and methodologies for formal specifications and proofs, part of the Microsoft Research-INRIA joint centre, since 2006.
  • The Caml Consortium.

Previous grants

  • U3CAT (static analysis and deductive verification of critical software written in C), ANR-08-ARPEGE, 2008-2012.
  • ASCERT (high-assurance static analyzers), Fondation de Recherche pour l'Aéronautique et l'Espace, 2009-2011.
  • Metal (typed metaprogramming), Digiteo, 2008-2010
  • Hisseo (semantics and static analysis of floating-point computations), Digiteo, 2008-2011.
  • Compcert (formal verification of compilers), coordinator, ANR ARA SSIA, 2005-2008.
  • ReFLect over OCaml (implementation of a domain-specific language), with Intel Corporation, 2005-2008.
  • EDOS (environment for the distribution of Open Source Software), European FP6 STREP, 2004-2007.
  • Modulogic (environment for the development of high-assurance software), ACI SI, 2003-2006.
  • Applied Semantics II, European Esprit working group, 2003-2006.