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é: 2024

Auteurs:

  • Paul Bonnot
  • Benoît Boyer
  • Florian Faissole
  • Claude Marché
  • Raphaël Rieu-Helft
Lire la publication