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)

Publications

Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function

Published: 2024

Authors:

  • Paul Bonnot
  • Benoît Boyer
  • Florian Faissole
  • Claude Marché
  • Raphaël Rieu-Helft
Read Publication