formal_methods.md

# 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. -->