Ongoing projects
- As part of the ProofInUse Consortium:
- Bilateral contract with TrustInSoft company (2020-2024)
- Bilateral contract with Mitsubishi Electric R&D Centre-Europe (2019-2024)
- Bilateral contract with AdaCore company (2019-2023)
- EMC2: Extreme-scale Mathematically-based Computational Chemistry (ERC Synergy projet, 2019-2026)
- FRESCO: Fast and Reliable Symbolic Computation (ERC Consolidator grant, 2021-2026)
- NuSCAP: Numerical Safety for Computer-Aided Proofs (ANR, 2021-2025)
- GOSPEL
: Vers un langage de spécification et un écosystème pour spécifier,
tester et vérifier des programmes OCaml (ANR PRCE, 2022-2026)
- Défi Inria
Liberabaci: Enseigner les mathématiques à l'aide de Coq
- Project Secureval of PEPR Cybersécurité (2022-2027)
- Project Décysif: Formal
Verification for Safety and Security, co-funded by French government
and Ile-de-France region, under the i-Demo call of plan de relance
France 2030.
Former projects
- PARDI: Verification of parameterized distributed systems (ANR, 2016-2021)
- VOCaL: The Verified OCaml Library (ANR, 2015-2021)
- CoLiS: Correction of Linux Scripts (ANR, 2015-2021)
- LCHIP: Low Cost High Integrity Platform (FUI, 2016-2019)
- ELEFFAN: (DigiCosme, 2016-2019)
- SOPRANO: A new automatic prover for static analysis of programs (ANR, 2014-2018)
- FastRelax: Fast and reliable approximation algorithms (ANR, 2014-2018)
- ProofInUse Joint Laboratory with AdaCore (ANR, programme LabCom, 2014-2017)
- ELFIC: Eléments finis certifiés (DigiCosme, 2014-2016)
- Deepsea: Parallel dynamic computations (ERC, 2013-2018)
- AJACS: JavaScript applications: certified analyses and security (ANR, 2014-2018)
- CAFEIN: Combining Analyses for the Study of Numerical Invariants (ANR, 2012-2016)
- BWare: Framework for automated verification of B proof obligations (ANR, programme Ingénierie Numérique & Sécurité, 2012-2016)
- Verasco: Verified Static Analyzers and Compilers (ANR, 2011-2015)
- Coquelicot New
real numbers for Coq (Digiteo 2011-2014)
- Hi-Lite Popularizing formal methods for the development of high-integrity software (FUI project, 2010-2013)
- ALT-ERGO Maturation du prouveur Alt-Ergo (INRIA ADT, 2009-2012)
- DECERT Deduction and Certification (ANR, 2009-2012)
- GENCOD
- SIESTA
- Action d'Envergure SYNCHRONICS
- COST european project: Verification of Object-Oriented Software
(03/2008-02/2012)
- HISSEO Verification of Floating-Point Programs (Digiteo
09/2008-02/2012)
- FOST Formal prOofs
about Scientific compuTations (ANR Programme Blanc, 2009-2012)
- U3CAT Unification of Critical C Codes Analysis Techniques (ANR Arpège 08, 01/2009-09/2012)
- SCALP Security of Cryptographic ALgorithms with Probabilities (ANR SESUR, 2008-2011)
- Cepromi Certification de Programmes Manipulant la Mémoire (INRIA ARC, 01/2008-12/2009)
- A3PAT Assister automatiquement les assistants de
preuve avec des traces (ANR Programme Blanc 12/2005-12/2008)
- CAT C Analysis Toolbox (ANR RNTL 01/2006-12/2008)
- CERPAN Certification de Programmes numériques (ANR Programme Blanc, 12/2005-12/2008)
- PFC Plate-forme de Confiance (FCE 01/2007-06/2009, competitive cluster System@tic)
- TYPES (European Coordination Action 09/2004-04/2008)
- ALIDECS
- GECCOO Génération de code certifié pour des applications orientées objet
Spécification, raffinement, preuve et détection d'erreurs (ACI Sécurité, 07/2003-12/2006)
- AVERROES Vérification de propriétés
quantitatives et fonctionnelles (RNTL 09/2002-03/2006)
- VERIFICARD tool-assisted specification and verification of JavaCard programs (European IST project 01/2001-09/2003)