Merge pull request #33 from Decysif/deliv_3_1

add deliverable 3.1
Decysif · Feb 12, 2025 · 529cff4 · 529cff4
2 parents 1546d19 + 3694041
commit 529cff4
Show file tree

Hide file tree

Showing 4 changed files with 37 additions and 3 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/layouts/page/deliverables.html b/layouts/page/deliverables.html
@@ -53,10 +53,18 @@ <h5 class="f6 fw6 dark-blue">{{ .id }} - {{ .name }}</h5>
                 {{ end }}
               </ul>
               <a href="{{ .pdf_url }}" class="link dim blue underline f6 fw5" target="_blank">
-                {{ if eq $parent.Site.Language.Lang "fr" }}
-                  Télécharger la version PDF
+                {{ if eq .id "L3.1" }}
+                  {{ if eq $parent.Site.Language.Lang "fr" }}
+                    Télécharger la version PDF (Anglaise)
+                  {{ else }}
+                    Download PDF version
+                  {{ end }}
                 {{ else }}
-                  Download PDF version (French)
+                  {{ if eq $parent.Site.Language.Lang "fr" }}
+                    Télécharger la version PDF
+                  {{ else }}
+                    Download PDF version (French)
+                  {{ end }}
                 {{ end }}
               </a>
             </div>

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