Skip to content

Commit

Permalink
Merge pull request #3 from Ninjapouet/master
Browse files Browse the repository at this point in the history
Fixed #2: adding minimal site informations.
  • Loading branch information
claudemarche authored Feb 9, 2024
2 parents ba8a97a + a5e59b8 commit 1a6db98
Show file tree
Hide file tree
Showing 14 changed files with 223 additions and 3 deletions.
4 changes: 4 additions & 0 deletions assets/sass/main.scss
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
p {
text-align: justify;
text-justify: auto;
}
12 changes: 12 additions & 0 deletions content/_index.en.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
---
title: "DéCySif"

description: "Formal verification in the service of safety"
cascade:
featured_image: '/images/gohugo-default-sample-hero-image.jpg'
---

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. Its objective is to improve the safety and security of critical
systems using formal verification tools.
12 changes: 12 additions & 0 deletions content/_index.fr.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
---
title: "DéCySif"

description: "La vérification formelle au service de la sécurité et la sûreté"
cascade:
#featured_image: '/images/gohugo-default-sample-hero-image.jpg'
featured_image: '/images/Decysif.png'
---

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.
40 changes: 40 additions & 0 deletions content/about.fr.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,40 @@
---
title: "À propos"
description: "Les acteurs du projet DéCySif"
featured_image: ''
menu:
main:
weight: 1
_build:
list: never
---

# Le projet

Depuis quelques années, le langage de programmation Rust vient concurrencer les
langages Ada/C/C++ établis dans le monde des logiciels critiques, embarqués ou
non. Les acteurs actuels et futurs développant des
logiciels critiques en Rust se posent désormais la question de l'opportunité
d'utiliser des outils d’analyse formelle pour Rust.

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
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
prouveur Alt-Ergo d'OCamlPro.

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.

{{< figure src="/images/Organisation-outils.png" >}}

# Le consortium

{{< presentation >}}

# Coordinateur

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" >}}).

16 changes: 16 additions & 0 deletions content/contact.fr.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,16 @@
---
title: Contact
featured_image: ''
omit_header_text: true
description: Laissez-nous un message!
type: page
menu: main
# _build:
# list: never

---

Pour nous contacter, merci de remplir le formulaire ci-dessous.

{{< form-contact >}}

Binary file added content/images/Decysif.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added content/images/Organisation-outils.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
Binary file added content/images/decysif_background.png
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
60 changes: 60 additions & 0 deletions data/consortium.yaml
Original file line number Diff line number Diff line change
@@ -0,0 +1,60 @@
- 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.
28 changes: 25 additions & 3 deletions hugo.toml
Original file line number Diff line number Diff line change
@@ -1,5 +1,27 @@
baseURL = 'https://decysif.fr'
languageCode = 'en-us'
title = 'DeCySif Project'
languageCode = 'fr'
title = 'DéCySif'
copyright = 'OCamlPro'

theme = 'ananke'

DefaultContentLanguage = "fr"

[languages]

[languages.fr]
weight = 1
[languages.fr.params]
legal = "DéCySif est financé par l'appel à projet i-Démo et la région Ile-de-France."

[languages.en]
weight = 2
disabled = true
[languages.en.params]
legal = "DéCySif is a project funded by the i-Démo call and the Ile-de-France region."

[params]
text_color = ""
[params.contact]
development = "https://formspree.io/f/mayreylq"

theme = 'ananke'
4 changes: 4 additions & 0 deletions layouts/partials/head-additions.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,4 @@
{{ $opts := dict "transpiler" "libsass" "targetPath" "css/style.css" }}
{{ with resources.Get "sass/main.scss" | toCSS $opts | minify | fingerprint }}
<link rel="stylesheet" href="{{ .RelPermalink }}" integrity="{{ .Data.Integrity }}" crossorigin="anonymous">
{{ end }}
9 changes: 9 additions & 0 deletions layouts/partials/site-footer.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
<footer class="{{ .Site.Params.background_color_class | default "bg-black" }} bottom-0 w-100 pa3" role="contentinfo">
<div class="justify-start">
<a class="f4 fw4 hover-white no-underline white-70 dn dib-ns pv2 ph3" href="{{ .Site.Home.Permalink }}" >
&copy; {{ with .Site.Copyright | default .Site.Title }} {{ . | safeHTML }} {{ now.Format "2006"}} {{ end }}
</a>
<div class="center f5 fw5 hover-white no-underline white-70 dn dib-ns pv2 ph3">{{ .Site.Param "legal" }}</div>
<div>{{ partial "social-follow.html" . }}</div>
</div>
</footer>
23 changes: 23 additions & 0 deletions layouts/shortcodes/form-contact.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,23 @@
{{ $.Scratch.Add "labelClasses" "f6 b db mb1 mt3 sans-serif mid-gray" }}
{{ $.Scratch.Add "inputClasses" "w-100 f5 pv3 ph3 bg-light-gray bn" }}
{{ $url := or (and hugo.IsProduction .Site.Params.Contact.production) .Site.Params.Contact.development }}

{{ with $url }}
<form class="black-80 sans-serif" accept-charset="UTF-8" action="{{ $url }}" method="POST" role="form">

<label class="{{ $.Scratch.Get "labelClasses" }}" for="name">{{ i18n "yourName" }}</label>
<input type="text" id="name" name="name" class="{{ $.Scratch.Get "inputClasses" }}" required placeholder=" " aria-labelledby="name"/>

<label class="{{ $.Scratch.Get "labelClasses" }}" for="email">{{ i18n "emailAddress" }}</label>
<input type="email" id="email" name="email" class="{{ $.Scratch.Get "inputClasses" }}" required placeholder=" " aria-labelledby="email"/>
<div class="requirements f6 gray glow i ph3 overflow-hidden">
{{ i18n "emailRequiredNote" }}
</div>

<label class="{{ $.Scratch.Get "labelClasses" }}" for="message">{{ i18n "message" }}</label>
<textarea id="message" name="message" class="{{ $.Scratch.Get "inputClasses" }} h4" aria-labelledby="message"></textarea>

<input class="db w-100 mv2 white pa3 bn hover-shadow hover-bg-black bg-animate bg-black" type="submit" value="{{ i18n "send" }}" />

</form>
{{ end }}
18 changes: 18 additions & 0 deletions layouts/shortcodes/presentation.html
Original file line number Diff line number Diff line change
@@ -0,0 +1,18 @@
<div class="flex flex-column">
{{ range $.Site.Data.consortium }}
<article class="center bg-white br3 pa3 pa4-ns mv3 ba b--black-10">
<div class="tc center">
{{/* <img src="http://tachyons.io/img/avatar_1.jpg" class="br-100 h3 w3 dib" title="Photo of a kitty staring at you"> */}}
<h1 class="f4">{{ .name }}</h1>
<hr class="mw3 bb bw1 b--black-10">
</div>
<p class="lh-copy measure center f6 black-70 tj">
{{ .description | transform.Markdownify }}
</p>
<div class="tc center">
<hr class="mw3 bb bw1 b--black-10">
<a class="f6 link dim br3 ph3 pv2 mb2 dib white bg-light-gray" href="{{ .url }}">{{ .url }}</a>
</div>
</article>
{{ end }}
</div>

0 comments on commit 1a6db98

Please sign in to comment.