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

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: