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ôt

L1.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)
Télécharger la version PDF
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)
Télécharger la version PDF

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
Lire la publication

Generating and Certifying Accuracy Properties of Floating-Point Programs

Publié: Inria Research Report, 2024

Auteurs:

  • Paul Bonnot
  • Benoît Boyer
  • Florian Faissole
  • Claude Marché
Lire la publication

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
Lire la publication

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
Lire la publication