Livrables
Le projet DéCySif fourni un cadre pour que le consortium puisse aboutir à un ensemble de livrables ainsi qu'une suite de papiers scientifiques divers qui seront réunis ci-dessous à mesure qu'ils voient le jour.
Livrables du projet
DépôtL1.1 - Constitution d’une base de fichiers d’entrée représentatifs des difficultés rencontrées pour générer des exploits.
Abstract: Ce livrable est constitué d’une base de tests qui se trouve dans le dépôt ’benchmarks’ du projet Décysif. Les objectifs du livrable sont d'identifier des faiblesses lors de la reconstruction d’un contre-exemple par Why3 depuis les modèles des solveurs SMT, ou les faiblesses des procédures de vérification et de catégorisation des contre-exemples.
Dirigé par: TrustInSoft
Auteurs:
- Guillaume Cluzel (TrustInSoft)
- Matteo Manighetti (Inria & Université Paris-Saclay)
- Claude Marché (Inria & Université Paris-Saclay)
- Yannick Moy (AdaCore)
L2.1 - Constitution d’une base de fichiers d’entrée représentatifs des difficultés rencontrées pour la preuve automatique.
Abstract: Ce livrable est constitué d’une base de tests qui se trouve dans le dépôt ’benchmarks’ du projet Décysif, dont les objectifs sont de repérer les faiblesses du prouveur Alt-Ergo, de repérer les problèmes de traduction (ou repérer des problèmes au niveau de l’écriture des théories, par exemple le modèle mémoire de J3) pour tous les prouveurs CVC5, CVC4, Z3, Alt-Ergo.
Dirigé par: AdaCore
Auteurs:
- Yannick Moy (AdaCore)
- Guillaume Cluzel (TrustInSoft)
- Matteo Manighetti (Inria & Université Paris-Saclay)
- Claude Marché (Inria & Université Paris-Saclay)
Publications
Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function
Publié: Formal Methods in Computer-Aided Design, 2024
Auteurs:
- Paul Bonnot
- Benoît Boyer
- Florian Faissole
- Claude Marché
- Raphaël Rieu-Helft
Generating and Certifying Accuracy Properties of Floating-Point Programs
Publié: Inria Research Report, 2024
Auteurs:
- Paul Bonnot
- Benoît Boyer
- Florian Faissole
- Claude Marché
Remonter les barrières pour ouvrir une clôture
Publié: 36es Journées Francophones des Langages Applicatifs, 2025
Auteurs:
- Paul Patault
- Arnaud Golfouse
- Xavier Denis
Faire chauffer Why3 avec de l’induction
Publié: 36es Journées Francophones des Langages Applicatifs, 2025
Auteurs:
- Henri Saudubray
- Jean-Christophe Filliâtre
- Andrei Paskevich