Commit 7ac9b385 authored by Julien Blond's avatar Julien Blond
Browse files

First draft of formal method page

parent 2484cf85
# 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
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
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
in various languages:
- safety requirements in C <!-- [JB] can we mention MERCE and/or the related project? -->
- 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. -->
......@@ -29,6 +29,9 @@
<li class="nav-item">
<a class="nav-link" href="/research-and-development">R&amp;D</a>
</li>
<li class="nav-item">
<a class="nav-link" href="/formal_methods">Formal Methods</a>
</li>
<li class="nav-item">
<a class="nav-link" href="/startup_studio">Startup Studio</a>
</li>
......
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