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)
L3.1 - Memory Models for Pointer Programs: a State of the Art from the Point of View of Décysif Partners
Abstract: L'objectif de ce document est de résumer les différents modèles mémoire implémentés dans les outils des partenaires Décysif, en mettant l'accent sur les choix de conception importants, et de les comparer brièvement entre eux et avec d'autres approches existantes dans la communauté internationale de la vérification déductive. À partir de ce résumé, nous dérivons et exposons certains travaux futurs que nous souhaitons réaliser dans le cadre du projet Décysif.
Dirigé par: Inria
Auteurs:
- Claude Marché (Inria & Université Paris-Saclay)
- Guillaume Cluzel (TrustInSoft)
- Claire Dross (AdaCore)
- Jean-Christophe Filliâtre (CNRS & Université Paris-Saclay)
- Jacques-Henri Jourdan (CNRS & Université Paris-Saclay)
- Andrei Paskevich (Université Paris-Saclay)
- Raphaël Rieu-Helft (TrustInSoft)
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