add deliverable 3.1

Decysif · Feb 4, 2025 · 6a9b767 · 6a9b767
1 parent 1546d19
commit 6a9b767
Show file tree

Hide file tree

Showing 3 changed files with 26 additions and 0 deletions.
diff --git a/content/en/deliverables.md b/content/en/deliverables.md
@@ -28,6 +28,19 @@ project_deliverables:
             - "Matteo Manighetti (Inria & Université Paris-Saclay)"
             - "Claude Marché (Inria & Université Paris-Saclay)"
           pdf_url: "/pdf/livrable_l2_1.pdf"
+        - id: "L3.1"
+          name: "Memory Models for Pointer Programs: a State of the Art from the Point of View of Décysif Partners"
+          synopsys: "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."
+          leader: "Inria"
+          authors:
+            - "Claude Marché (Inria & Université Paris-Saclay)"
+            - "Guillaume Cluzel (TrustInSoft)"
+            - "Claire Dross (AdaCore)"
+            - "Jean-Christophe Filliâtre (CNRS & Université Paris-Saclay)"
+            - "Jacques-Henri Jourdan (CNRS & Université Paris-Saclay)"
+            - "Andrei Paskevich (Université Paris-Saclay)"
+            - "Raphaël Rieu-Helft (TrustInSoft)"
+          pdf_url: "/pdf/livrable_l3_1.pdf"
 
 publications:
   - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function"

diff --git a/content/fr/deliverables.md b/content/fr/deliverables.md
@@ -28,6 +28,19 @@ project_deliverables:
             - "Matteo Manighetti (Inria & Université Paris-Saclay)"
             - "Claude Marché (Inria & Université Paris-Saclay)"
           pdf_url: "/pdf/livrable_l2_1.pdf"
+        - id: "L3.1"
+          name: "Memory Models for Pointer Programs: a State of the Art from the Point of View of Décysif Partners"
+          synopsys: "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."
+          leader: "Inria"
+          authors:
+            - "Claude Marché (Inria & Université Paris-Saclay)"
+            - "Guillaume Cluzel (TrustInSoft)"
+            - "Claire Dross (AdaCore)"
+            - "Jean-Christophe Filliâtre (CNRS & Université Paris-Saclay)"
+            - "Jacques-Henri Jourdan (CNRS & Université Paris-Saclay)"
+            - "Andrei Paskevich (Université Paris-Saclay)"
+            - "Raphaël Rieu-Helft (TrustInSoft)"
+          pdf_url: "/pdf/livrable_l3_1.pdf"
 
 publications:
   - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function"

diff --git a/static/pdf/livrable_l3_1.pdf b/static/pdf/livrable_l3_1.pdf