Commit 5f4da0be authored by Julien Blond's avatar Julien Blond
Browse files

Added links, certification and partnership

parent 7ac9b385
<!-- Link definitions -->
[Alt-Ergo]: https://alt-ergo.ocamlpro.com
[Why3]: http://why3.lri.fr
[Frama-C]: https://frama-c.com
[SPARK]: https://www.adacore.com/sparkpro
[Common Criteria]: https://www.commoncriteriaportal.org/
[B]: https://www.atelierb.eu/
[CEA List]: http://www-list.cea.fr/
[MERCE]: https://www.mitsubishielectric-rce.eu/
[INRIA]: https://www.inria.fr/fr
[Adacore]: https://www.adacore.com/
[TrustInSoft]: https://trust-in-soft.com/
[Dolmen]: https://github.com/Gbury/dolmen
# Formal Methods
<!-- [JB] Only content for now. Maybe add an intro ? -->
## Alt-Ergo
Alt-Ergo is an open-source automatic solver based on Satisfiability Modulo
Theories (SMT). Successfully designed for proving formulas generated in the
[Alt-Ergo] is an open-source automatic solver
based on Satisfiability Modulo Theories (SMT). Successfully designed for
proving formulas generated in the
context of deductive program verification.
It is mostly used as a back-end of different program verification tools via
the Why3 platform like Frama-C for C or SPARK for Ada. Alt-Ergo is also used
to prove formulas issued from B modelizations and from cryptographic protocols
the [Why3] platform like [Frama-C]
for C or [SPARK] for Ada. [Alt-Ergo] is also used
to prove formulas issued from [B] modelizations and from cryptographic protocols
verification.
<!-- [JB] I would be nice to promote such work but i don't know if it can be considered
as a formal method work? By the way do we contribute to other stuff like that ? -->
<!-- As Alt-Ergo maintainers, we also promote its evolution by contributing to
projects like Dolmen. -->
## Program Verification
We developped several static analysis enforcing security or safety properties
......@@ -25,3 +39,26 @@ in various languages:
- OCaml exceptions tracking <!-- [JB] add SecureOCaml FUI link? -->
- reaching unspecified or breaking invariant states in transition system based languages <!-- [JB] GEHC is under NDA so we can't talk explicitly about it but we may link to mikino/verification for dummies. -->
## Certification
High assurance level in [Common Criteria] certification implies the formalization
of at least the security policy model corresponding to the family SPM. Such
formalization is usually expensive and subcontracting it lower both the risk
and costs.
Our experienced R&D team can deal with it and help your products reaching the
EAL 6 or 7 certification.
## Partnership
We are involved in formal methods related partnership:
- [INRIA]
- [CEA List]
- [MERCE]
- [Adacore]
- [TrustInSoft]
- <!-- [JB] More ?-->
In addition, we contribute to open-source tooling:
- [Dolmen]: a generic front-end for solvers
- <!-- [JB] What else ? -->
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment