Software
Program Verification
- CFML is a tool that allows to verify the full functional correctness of OCaml programs. Proofs are conducted interactively, within the Coq proof assistant. CFML, which is based on the technique of "characteristic formulae", has been used to verify a collection of data structures and algorithms.
- Creusot: an environment for deductive verification of Rust programs
- Cubicle: an SMT-based model checker for parameterized systems
- Frama-C: Environment for Static Analysis of C source, developed in collaboration with CEA-List and now mainly developed and maintained by CEA
- SPARK2014: Environment for the safe development of critical applications in Ada, developed by AdaCore. We contribute to the proof tool of SPARK2014, in the context of the ProofInUse common laboratory.
- Why3: A multi-input multi-prover verification platform
Automated Deduction
- Alt-Ergo: automatic prover modulo theories term rewriting toolbox
- Gappa is a tool for automatically verifying properties on numerical programs dealing with floating-point or fixed-point arithmetic. While it is intended to be used directly, it can also act as a backend prover for the Why platform or as an automatic tactic for the Coq proof assistant.
Objective Caml libraries and tools
- bibtex2html: generation of HTML pages from bibliographies
- Ocamlgraph: Objective Caml library for graphs
- Mlpost: Ocaml front-end for producing figures
Coq Libraries
- ALEA: a Coq library for reasoning on randomized algorithms
- Coccinelle: a Coq library for term rewriting systems
- Coq.Interval provides a Coq tactic for automatically proving some inequalities between real-valued expressions containing elementary functions.
- Coquelicot Coquelicot is a Coq library dedicated to real analysis: differentiation, integration, and so on. It is a conservative extension of the standard library of Coq, but with a strong focus on usability.
- Flocq (Floats for Coq) is a formalization of floating-point arithmetic for the Coq system. It provides a comprehensive library of theorems on a multi-radix multi-precision arithmetic; it also supports efficient numerical computations inside Coq.
- PFF: a Coq library on floating-point arithmetic