add paper listing, fix typos, add en/fr switch when in single blogpos…

…t page
Decysif · Aug 27, 2024 · df4666f · df4666f
1 parent d9d0f5c
commit df4666f
Show file tree

Hide file tree

Showing 9 changed files with 250 additions and 159 deletions.
diff --git a/assets/sass/main.scss b/assets/sass/main.scss
@@ -3,6 +3,11 @@ p {
     text-justify: auto;
 }
 
+.pv5 {
+    padding-top: 1rem;
+    padding-bottom: 1rem;
+}
+
 #sitelogo {
     max-width: 15rem ;
 }
diff --git a/content/en/_index.md b/content/en/_index.md
@@ -5,7 +5,7 @@ cascade:
   featured_image: '/images/Decysif.png'
 description: "Formal verification in the service of safety and security"
 synopsis: "DéCySif is a regional R&D project funded by an i-Démo call and the
-Ile-de-France French region gathering Adacore, INRIA, OCamlPro and TrustInSoft.
+Ile-de-France French region gathering AdaCore, Inria, OCamlPro and TrustInSoft.
 Its objective is to improve the safety and security of critical systems using
 formal verification tools."
 
@@ -18,10 +18,10 @@ project:
   tools for Rust.
   <br />
   <br />
-  It is as a direct answer to that question that INRIA have developped Creusot, a
+  It is as a direct answer to that question that Inria have developped Creusot, a
   tool for Rust. The tool itself is based off the same technological foundations
   as AdaCore's and TrustInSoft's formal analysis tools: the Why3 platform,
-  developped by INRIA, and a collections of SMT-Solvers such as Alt-Ergo,
+  developped by Inria, and a collections of SMT-Solvers such as Alt-Ergo,
   developped by OCamlPro.
   <br />
   <br />
@@ -39,63 +39,9 @@ coordinator:
   content: "TrustInSoft are the coordinators of the project. For any enquiry,
   please use the [contact form]({{< ref \"contact.en.md\" >}})."
 
-
-collaborators:
-  sectiontitle: "The consortium"
-  consortium:
-    - name: "Adacore"
-      url: "https://www.adacore.com/"
-      description:
-        "Founded in 1994, AdaCore designs and provides software development and
-        verification tools for applications where safety, security, and reliability
-        are critical elements.<br />
-        The use of AdaCore products continues to grow in critical applications such
-        as space systems, commercial avionics, military systems, air traffic
-        control, railway systems, medical devices, or financial services. AdaCore
-        enjoys a substantial and constantly growing base of international clients;
-        visit www.adacore.com/industries/ for more information.<br />
-        AdaCore products are free and come with expert online support provided by
-        the developers themselves. The company has a North American headquarters
-        based in New York and a European headquarters based in Paris."
-
-    - name: "INRIA - LMF - Toccata"
-      url: "https://www.inria.fr/en/toccata"
-      description: 
-        "The [INRIA](https://www.inria.fr) is the French national public institute
-        for research in computer science. The INRIA members of the DéCySif project
-        belong to the Formal Methods Laboratory ([LMF](https://lmf.cnrs.fr/))
-        and the Toccata research team
-        ([Toccata](http://toccata.gitlabpages.inria.fr/toccata/)), located in
-        Orsay, France; and jointly affiliated with the University of
-        Paris-Saclay, CNRS, and the INRIA Saclay - Île-de-France research
-        center.
-        <br />
-        The general objective of the team is to promote formal specifications
-        and computer-assisted proofs in the development of software requiring a
-        high level of confidence in their safety and adherence to expected
-        behaviors."
-
-    - name: "OCamlPro"
-      url: "https://www.ocamlpro.com"
-      description:
-        "OCamlPro is an R&D consulting firm specializing in engineering problems
-        related to programming languages, business-specific requirements, or
-        technical debt. The company is committed to open source and contributes to
-        the Rust, WebAssembly, and OCaml languages. The company also develops the
-        Alt-Ergo SMT solver used in DéCySif.<br />
-        OCamlPro is also active in the field of Common Criteria certification at
-        the EAL6 level and the use of formal methods (Coq, Lean4, Why3)."
-
-    - name: "TrustInSoft"
-      url: "https://trust-in-soft.com/"
-      description:
-        "TrustInSoft markets tools and services for exhaustive analysis of C and C++
-        source code, providing mathematical guarantees on the quality of their
-        clients' software. These software analysis solutions ensure the security
-        and reliability of source code without altering the development process.
-        These offerings are deployed worldwide among developers and integrators of
-        software components from the aerospace, automotive, railway, military,
-        nuclear, telecoms, or IoT industries."
+publications:
+  - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function"
+    url: "https://inria.hal.science/hal-04674600"
 
 software:
   sectiontitle: "Our softwares"
@@ -144,7 +90,7 @@ software:
       polymorphism, its compatibility with the SMT2 format, and several
       theories that allow it to formally handle basic types. The Alt-Ergo Club
       brings together a group of industrials (Thales, MERCE, Trust In Soft,
-      Adacore, etc.) using Alt-Ergo in their activities and helps to fund the
+      AdaCore, etc.) using Alt-Ergo in their activities and helps to fund the
       evolution of Alt-Ergo."
 
     - name: "SPARK, an industrial tool for deductive verification of the Ada language."
@@ -169,4 +115,61 @@ software:
       url:
         - "https://www.trust-in-soft.com/trustinsoft-analyzer"
       description: "Soon..."
+
+collaborators:
+  sectiontitle: "The consortium"
+  consortium:
+    - name: "AdaCore"
+      url: "https://www.adacore.com/"
+      description:
+        "Founded in 1994, AdaCore designs and provides software development and
+        verification tools for applications where safety, security, and reliability
+        are critical elements.<br />
+        The use of AdaCore products continues to grow in critical applications such
+        as space systems, commercial avionics, military systems, air traffic
+        control, railway systems, medical devices, or financial services. AdaCore
+        enjoys a substantial and constantly growing base of international clients;
+        visit www.adacore.com/industries/ for more information.<br />
+        AdaCore products are free and come with expert online support provided by
+        the developers themselves. The company has a North American headquarters
+        based in New York and a European headquarters based in Paris."
+
+    - name: "Inria - LMF - Toccata"
+      url: "https://www.inria.fr/en/toccata"
+      description: 
+        "The [Inria](https://www.inria.fr) is the French national public institute
+        for research in computer science. The Inria members of the DéCySif project
+        belong to the Formal Methods Laboratory ([LMF](https://lmf.cnrs.fr/))
+        and the Toccata research team
+        ([Toccata](http://toccata.gitlabpages.inria.fr/toccata/)), located in
+        Orsay, France; and jointly affiliated with the University of
+        Paris-Saclay, CNRS, and the Inria Saclay - Île-de-France research
+        center.
+        <br />
+        The general objective of the team is to promote formal specifications
+        and computer-assisted proofs in the development of software requiring a
+        high level of confidence in their safety and adherence to expected
+        behaviors."
+
+    - name: "OCamlPro"
+      url: "https://www.ocamlpro.com"
+      description:
+        "OCamlPro is an R&D consulting firm specializing in engineering problems
+        related to programming languages, business-specific requirements, or
+        technical debt. The company is committed to open source and contributes to
+        the Rust, WebAssembly, and OCaml languages. The company also develops the
+        Alt-Ergo SMT solver used in DéCySif.<br />
+        OCamlPro is also active in the field of Common Criteria certification at
+        the EAL6 level and the use of formal methods (Coq, Lean4, Why3)."
+
+    - name: "TrustInSoft"
+      url: "https://trust-in-soft.com/"
+      description:
+        "TrustInSoft markets tools and services for exhaustive analysis of C and C++
+        source code, providing mathematical guarantees on the quality of their
+        clients' software. These software analysis solutions ensure the security
+        and reliability of source code without altering the development process.
+        These offerings are deployed worldwide among developers and integrators of
+        software components from the aerospace, automotive, railway, military,
+        nuclear, telecoms, or IoT industries."
 ---
diff --git a/content/en/post/00_kickoff_of_project_decysif.md b/content/en/post/00_kickoff_of_project_decysif.md
@@ -9,7 +9,7 @@ title: "Formal Cyber-Security Diagnostic: DéCySif"
 
 On Tuesday, December 19, 2023, all partners of the Decysif project
 ([TrustInSoft](https://trust-in-soft.com/),
-[Adacore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com), and
+[AdaCore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com), and
 the [LMF](https://lmf.cnrs.fr/) team) gathered at the TrustInSoft offices in
 the 14th arrondissement of Paris for the project kickoff meeting!
 

diff --git a/content/fr/_index.md b/content/fr/_index.md
@@ -4,8 +4,8 @@ sectiontitle: "Accueil"
 cascade:
   featured_image: '/images/Decysif.png'
 description: "La vérification formelle au service de la sécurité et la sûreté"
-synopsis: "DéCySif est un projet i-Demo régional de R&D regroupant Adacore,
-l'INRIA, OCamlPro et TrustInSoft. Il vise à améliorer la sécurité et la sûreté
+synopsis: "DéCySif est un projet i-Demo régional de R&D regroupant AdaCore,
+l'Inria, OCamlPro et TrustInSoft. Il vise à améliorer la sécurité et la sûreté
 des systèmes critiques en utilisant des outils de vérification formelle."
 
 project:
@@ -18,9 +18,9 @@ project:
   <br />
   <br />
   C'est pour répondre à cette question que l'outil Creusot pour Rust a été
-  développé par l'INRIA. L'outil est basé sur les mêmes fondations technologiques
+  développé par l'Inria. L'outil est basé sur les mêmes fondations technologiques
   que les outils d’analyse formelle d’AdaCore et de TrustInSoft : la plateforme
-  Why3 développée par l'INRIA et les mêmes prouveurs automatiques dont le
+  Why3 développée par l'Inria et les mêmes prouveurs automatiques dont le
   prouveur Alt-Ergo d'OCamlPro.
   <br />
   <br />
@@ -37,66 +37,9 @@ coordinator:
   content: "La société TrustInSoft est le coordinateur du projet. Pour toute
   demande d'information, veuillez passer par le formulaire de [contact]({{< ref \"contact.fr.md\" >}})."
 
-collaborators:
-  sectiontitle: "Le consortium"
-  consortium:
-    - name: "Adacore"
-      url : "https://www.adacore.com/"
-      description:
-        "Fondée en 1994, AdaCore conçoit et fournit des outils de développement et
-        de vérification de logiciels destinés à des applications pour lesquelles la
-        sûreté, la sécurité et la fiabilité sont des éléments critiques.<br />
-        L'utilisation des produits AdaCore connaît une croissance continue dans des
-        applications critiques telles que les systèmes spatiaux, l'avionique
-        commerciale, les systèmes militaires, le contrôle aérien, les systèmes
-        ferroviaires, les appareils médicaux ou les services financiers. AdaCore
-        jouit d'une base fournie de clients internationaux en croissance
-        constante; visitez le site www.adacore.com/industries/ pour de plus amples
-        informations.<br />
-        Les produits AdaCore sont libres et accompagnés d'un support expert en
-        ligne fourni par les développeurs eux-mêmes. La société possède un siège
-        nord-américain basé à New York et un siège européen basé à Paris."
-
-    - name: "INRIA - LMF - Toccata"
-      url: "https://www.inria.fr/fr/toccata"
-      description:
-        "L'[INRIA](https://www.inria.fr) est l'institut national public
-        français de recherche en sciences de l'informatique. Les membres INRIA
-        du projet DéCySif appartiennent au Laboratoire Méthodes Formelles
-        ([LMF](https://lmf.cnrs.fr/)) et à l'équipe de recherche
-        [Toccata](http://toccata.gitlabpages.inria.fr/toccata/), localisés à
-        Orsay, France ; et communs à l'Université Paris-Saclay, au CNRS, et au
-        centre de recherche INRIA Saclay - Île-de-France.
-        <br />
-        L'objectif général de l'équipe est de promouvoir les spécifications
-        formelles et les preuves assistées par ordinateur dans le cadre du
-        développement de logiciels requérant un haut niveau de confiance dans
-        leur sûreté de fonctionnement et le respect de comportements attendus."
-
-    - name: "OCamlPro"
-      url: "https://www.ocamlpro.com"
-      description: 
-        "OCamlPro est un cabinet d'étude en R&D spécialisé dans les problèmes
-        d'ingénieurie liés aux langages de programmation, aux spécificités métiers
-        ou à la dette technique. La société est engagée dans l'*open source*
-        et contribue aux langages Rust, WebAssembly et OCaml. La société développe
-        aussi le prouveur SMT Alt-Ergo utilisé dans DéCySif.<br />
-        OCamlPro est également active dans le domaine de la certification
-        Critères Communs au niveau EAL6 et l'utilisation des méthodes formelles
-        (Coq, Lean4, Why3)."
-
-
-    - name: "TrustInSoft"
-      url: "https://trust-in-soft.com/"
-      description: 
-        "TrustInSoft commercialise des outils et services d'analyse exhaustive de
-        code source C et C++ permettant d'apporter des garanties mathématiques sur
-        la qualité des logiciels de ses clients. Ces solutions d'analyses de
-        logiciel permettent d'avoir des garanties sur la sécurité et la fiabilité
-        du code source sans modifier le processus de développement. Ces offres
-        sont déployées dans le monde entier chez les développeurs et intégrateurs
-        de composants logiciels issus des industries aéronautique, automobile,
-        ferroviaire, militaire, nucléaire, télécoms, ou l'IoT."
+publications:
+  - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function"
+    url: "https://inria.hal.science/hal-04674600"
 
 software:
   sectiontitle: "Les logiciels"
@@ -149,7 +92,7 @@ software:
       domaines, grâce à son support inné du polymorphisme, sa compatibilité
       avec le format SMT2 et plusieurs théories lui permettant de manipuler
       formellement les types de base. Le Club Alt-Ergo rassemble un groupe
-      d’industriels (Thales, MERCE, Trust In Soft, Adacore, etc.) utilisant
+      d’industriels (Thales, MERCE, Trust In Soft, AdaCore, etc.) utilisant
       Alt-Ergo dans leur activité et permet de financer l’évolution
       d’Alt-Ergo."
 
@@ -176,4 +119,65 @@ software:
       url:
         - "https://www.trust-in-soft.com/trustinsoft-analyzer"
       description: "Bientôt..."
+
+collaborators:
+  sectiontitle: "Le consortium"
+  consortium:
+    - name: "AdaCore"
+      url : "https://www.adacore.com/"
+      description:
+        "Fondée en 1994, AdaCore conçoit et fournit des outils de développement et
+        de vérification de logiciels destinés à des applications pour lesquelles la
+        sûreté, la sécurité et la fiabilité sont des éléments critiques.<br />
+        L'utilisation des produits AdaCore connaît une croissance continue dans des
+        applications critiques telles que les systèmes spatiaux, l'avionique
+        commerciale, les systèmes militaires, le contrôle aérien, les systèmes
+        ferroviaires, les appareils médicaux ou les services financiers. AdaCore
+        jouit d'une base fournie de clients internationaux en croissance
+        constante; visitez le site www.adacore.com/industries/ pour de plus amples
+        informations.<br />
+        Les produits AdaCore sont libres et accompagnés d'un support expert en
+        ligne fourni par les développeurs eux-mêmes. La société possède un siège
+        nord-américain basé à New York et un siège européen basé à Paris."
+
+    - name: "Inria - LMF - Toccata"
+      url: "https://www.inria.fr/fr/toccata"
+      description:
+        "L'[Inria](https://www.inria.fr) est l'institut national public
+        français de recherche en sciences de l'informatique. Les membres Inria
+        du projet DéCySif appartiennent au Laboratoire Méthodes Formelles
+        ([LMF](https://lmf.cnrs.fr/)) et à l'équipe de recherche
+        [Toccata](http://toccata.gitlabpages.inria.fr/toccata/), localisés à
+        Orsay, France ; et communs à l'Université Paris-Saclay, au CNRS, et au
+        centre de recherche Inria Saclay - Île-de-France.
+        <br />
+        L'objectif général de l'équipe est de promouvoir les spécifications
+        formelles et les preuves assistées par ordinateur dans le cadre du
+        développement de logiciels requérant un haut niveau de confiance dans
+        leur sûreté de fonctionnement et le respect de comportements attendus."
+
+    - name: "OCamlPro"
+      url: "https://www.ocamlpro.com"
+      description: 
+        "OCamlPro est un cabinet d'étude en R&D spécialisé dans les problèmes
+        d'ingénieurie liés aux langages de programmation, aux spécificités métiers
+        ou à la dette technique. La société est engagée dans l'*open source*
+        et contribue aux langages Rust, WebAssembly et OCaml. La société développe
+        aussi le prouveur SMT Alt-Ergo utilisé dans DéCySif.<br />
+        OCamlPro est également active dans le domaine de la certification
+        Critères Communs au niveau EAL6 et l'utilisation des méthodes formelles
+        (Coq, Lean4, Why3)."
+
+
+    - name: "TrustInSoft"
+      url: "https://trust-in-soft.com/"
+      description: 
+        "TrustInSoft commercialise des outils et services d'analyse exhaustive de
+        code source C et C++ permettant d'apporter des garanties mathématiques sur
+        la qualité des logiciels de ses clients. Ces solutions d'analyses de
+        logiciel permettent d'avoir des garanties sur la sécurité et la fiabilité
+        du code source sans modifier le processus de développement. Ces offres
+        sont déployées dans le monde entier chez les développeurs et intégrateurs
+        de composants logiciels issus des industries aéronautique, automobile,
+        ferroviaire, militaire, nucléaire, télécoms, ou l'IoT."
 ---
diff --git a/...t/fr/post/00_kickoff_du_projet_decysif.md → .../fr/post/00_kickoff_of_project_decysif.md b/...t/fr/post/00_kickoff_du_projet_decysif.md → .../fr/post/00_kickoff_of_project_decysif.md
@@ -9,7 +9,7 @@ title: "Diagnostic de Cyber-Sécurité Formel: DéCySif"
 
 Ce mardi 19 décembre 2023, tous les partenaires du projet Decysif
 ([TrustInSoft](https://trust-in-soft.com/),
-[Adacore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com) et
+[AdaCore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com) et
 l’équipe [LMF](https://lmf.cnrs.fr/)) se sont réunis dans les locaux de
 TrustInSoft dans le 14ème arrondissement de Paris pour la réunion de lancement
 du projet !

diff --git a/hugo.toml b/hugo.toml
@@ -26,7 +26,7 @@ Paginate = 10
       legal = "DéCySif is a project funded by the i-Démo call and the Ile-de-France region."
 
 [params]
-  site_logo = 'images/logo_decysif_excellence_for_security_blank_bg_rectangle.svg'
+  site_logo = '/images/logo_decysif_excellence_for_security_blank_bg_rectangle.svg'
   text_color = ""
   recent_posts_number = 5
 [params.contact]