Deliverables

The DéCySif project provides a framework for the consortium to produce a set of deliverables as well as a series of diverse scientific papers, which will be compiled below as they are published.

Project Deliverables

Repository

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: This deliverable consists of a test suite located in the 'benchmarks' repository of the Décysif project. The objectives of the deliverable are to identify weaknesses in the reconstruction of a counterexample by Why3 from SMT solver models, or in the procedures for verifying and categorizing counterexamples.

Led by: TrustInSoft

Authors:

Guillaume Cluzel (TrustInSoft)
Matteo Manighetti (Inria & Université Paris-Saclay)
Claude Marché (Inria & Université Paris-Saclay)
Yannick Moy (AdaCore)

Download PDF version (French)

L2.1 - Constitution d’une base de fichiers d’entrée représentatifs des difficultés rencontrées pour la preuve automatique.

Abstract: This deliverable consists of a test suite located in the 'benchmarks' repository of the Décysif project, with the objectives of identifying weaknesses in the Alt-Ergo solver, detecting translation issues (or identifying problems in the writing of theories, such as the memory model of J3) for all solvers: CVC5, CVC4, Z3, and Alt-Ergo.

Led by: AdaCore

Authors:

Yannick Moy (AdaCore)
Guillaume Cluzel (TrustInSoft)
Matteo Manighetti (Inria & Université Paris-Saclay)
Claude Marché (Inria & Université Paris-Saclay)

Download PDF version (French)

L3.1 - Memory Models for Pointer Programs: a State of the Art from the Point of View of Décysif Partners

Abstract: The purpose of this document is to summarize the different memory models implemented in the tools of the Décysif partners, focusing on the important design choices, and briefly compare them with each other and with other existing approaches in the international community of deductive verification. From such a summary, we derive and expose some future work we want to perform in the context of the Décysif project.

Led by: Inria

Authors: