From 5b47d2ec088e8167a1e05bd12e7c19b706a5baa2 Mon Sep 17 00:00:00 2001 From: RadioPotin Date: Mon, 26 Aug 2024 11:14:29 +0200 Subject: [PATCH] remove old consortium files, fix image links, make img alt language dependent --- content/en/_index.md | 8 +++++- content/fr/_index.md | 8 +++++- data/consortium_en.yaml | 50 ------------------------------------ data/consortium_fr.yaml | 56 ----------------------------------------- hugo.toml | 2 +- layouts/index.html | 2 +- 6 files changed, 16 insertions(+), 110 deletions(-) delete mode 100644 data/consortium_en.yaml delete mode 100644 data/consortium_fr.yaml diff --git a/content/en/_index.md b/content/en/_index.md index f33ba87..9885c6f 100644 --- a/content/en/_index.md +++ b/content/en/_index.md @@ -2,7 +2,7 @@ title: "DéCySif" sectiontitle: "Home" cascade: - featured_image: '/images/Decysif.png' + 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. @@ -28,6 +28,12 @@ project: Project DéCySif is the crucible for the improvement of all these tools and aims at guaranteeing convergence towards an optimal solution for the safety and security of embedded systems. " + img: + src: "images/Organisation-outils.png" + alt: "An image that shows the connections between the tools developed by + the actors of the DéCySif project. In the center, we see the Why3 platform, + and on the left side, the languages (Creusot, SPARK, TIS Analyzer) and the + Alt-Ergo prover on the right side." coordinator: sectiontitle: "Coordinator" diff --git a/content/fr/_index.md b/content/fr/_index.md index 42400d1..577ea2d 100644 --- a/content/fr/_index.md +++ b/content/fr/_index.md @@ -2,7 +2,7 @@ title: "DéCySif" sectiontitle: "Accueil" cascade: - featured_image: '/images/Decysif.png' + 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é @@ -26,6 +26,12 @@ project:
Le projet DéCySif vie l'amélioration de tous ces outils afin de converger vers une solution optimale pour la sécurité et la sûreté des systèmes critiques." + img: + src: "images/Organisation-outils.png" + alt: "Une image qui montre les liens entre les outils développés par les + acteurs du projet DéCySif. On voit au centre la platforme Why3 et, à + gauche, les langages utilisés (Creusot, SPARK, TIS Analyzer) et de l'autre + le prouveurs Alt-Ergo." coordinator: sectiontitle: "Coordinateur" diff --git a/data/consortium_en.yaml b/data/consortium_en.yaml deleted file mode 100644 index fcaf060..0000000 --- a/data/consortium_en.yaml +++ /dev/null @@ -1,50 +0,0 @@ -- 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/data/consortium_fr.yaml b/data/consortium_fr.yaml deleted file mode 100644 index dddd41d..0000000 --- a/data/consortium_fr.yaml +++ /dev/null @@ -1,56 +0,0 @@ -- 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/hugo.toml b/hugo.toml index 5522602..cdaaa87 100644 --- a/hugo.toml +++ b/hugo.toml @@ -25,7 +25,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/index.html b/layouts/index.html index 136598d..b1ea786 100644 --- a/layouts/index.html +++ b/layouts/index.html @@ -28,7 +28,7 @@

{{ .Params.project.content | markdownify}}
- Une image qui montre les liens entre les outils développés par les acteurs du projet DéCySif. On voit au centre la passerelle Why3 et de part et d'autre, les langages utilisés et les prouveurs que la passerelle instrumentalise. + {{ .Params.project.img.alt }}

{{ .Params.coordinator.sectiontitle }}