diff --git a/content/en/deliverables.md b/content/en/deliverables.md index 239ff75..7a53c2c 100644 --- 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 index 76232ed..32e2404 100644 --- 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 index ff48890..a29330e 100644 --- a/layouts/page/deliverables.html +++ b/layouts/page/deliverables.html @@ -53,10 +53,18 @@
{{ .id }} - {{ .name }}
{{ end }} - {{ 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 }} diff --git a/static/pdf/livrable_l3_1.pdf b/static/pdf/livrable_l3_1.pdf new file mode 100644 index 0000000..b903f88 Binary files /dev/null and b/static/pdf/livrable_l3_1.pdf differ