The ProVal team was stopped at the end of August 2012, and reborn into a new team
Toccata
These pages do not evolve anymore, please follow the link above for up-to-date informations about our team.
Projects
Ongoing projects
- ALT-ERGO Maturation du prouveur Alt-Ergo (INRIA ADT, 2009-2011)
- DECERT Deduction and Certification (ANR, 2009-2012)
- SCALP Security of Cryptographic ALgorithms with Probabilities (ANR SESUR, 2008-2011)
- COST european project: Verification of Object-Oriented Software (03/2008-02/2012)
- GENCOD
- SIESTA
- HISSEO Verification of Floating-Point Programs (Digiteo 09/2008-08/2011)
- FOST Formal prOofs about Scientific compuTations (ANR Programme Blanc, 2009-2012)
- Action d'Envergure SYNCHRONICS
- U3CAT Unification of Critical C Codes Analysis Techniques (ANR Arpège 08, 01/2009-12/2011)
- Coquelicot New real numbers for Coq (Digiteo 2011-2014)
Old projects
- 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)