diff --git a/assets/sass/main.scss b/assets/sass/main.scss
index f37ebb3..102cf34 100644
--- 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
index 94fd6cb..104983b 100644
--- 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.
- 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.
@@ -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.
- 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.
- 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.
-
- 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.
- 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.
+ 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.
+ 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.
+
+ 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.
+ 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
index 77b9522..a4b88ee 100644
--- 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
index 63feac7..5927081 100644
--- 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:
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.
@@ -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.
- 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.
- 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.
-
- 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.
- 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.
+ 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.
+ 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.
+
+ 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.
+ 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/content/fr/post/00_kickoff_du_projet_decysif.md b/content/fr/post/00_kickoff_of_project_decysif.md
similarity index 95%
rename from content/fr/post/00_kickoff_du_projet_decysif.md
rename to content/fr/post/00_kickoff_of_project_decysif.md
index b6e3815..d2a1305 100644
--- a/content/fr/post/00_kickoff_du_projet_decysif.md
+++ b/content/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
index 464928e..749fb4c 100644
--- 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]
diff --git a/layouts/_default/single.html b/layouts/_default/single.html
new file mode 100644
index 0000000..df8181b
--- /dev/null
+++ b/layouts/_default/single.html
@@ -0,0 +1,67 @@
+{{ define "header" }}
+ {{/* We can override any block in the baseof file be defining it in the template */}}
+ {{ partial "page-header.html" . }}
+{{ end }}
+{{ define "main" }}
+ {{ $section := .Site.GetPage "section" .Section }}
+
+
+
+ {{ partial "social-share.html" . }}
+
+ {{- .Title -}}
+
+ {{ with .Params.author | default .Site.Params.author }}
+
+ {{ end }}
+ {{/* Hugo uses Go's date formatting is set by example. Here are two formats */}}
+ {{ if not .Date.IsZero }}
+
+ {{end}}
+
+ {{/*
+ Show "reading time" and "word count" but only if one of the following are true:
+ 1) A global config `params` value is set `show_reading_time = true`
+ 2) A section front matter value is set `show_reading_time = true`
+ 3) A page front matter value is set `show_reading_time = true`
+ */}}
+ {{ if (or (eq (.Param "show_reading_time") true) (eq $section.Params.show_reading_time true) )}}
+ - {{ i18n "readingTime" .ReadingTime }}
+ - {{ i18n "wordCount" .WordCount }}
+ {{ end }}
+
+