- Why3: A multi-input multi-prover verification platform
- Why (version 2): the former
version of Why
(includes Krakatoa and the Jessie plug-in of Frama-C)
- Frama-C: Environment for Static Analysis of C source, developed in collaboration with CEA-List and now mainly 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.
- Alt-Ergo: automatic prover modulo theories
- CiME: term rewriting toolbox
- Cubicle: a Parallel SMT-based model checker for
- 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.
- Reactive ML: Synchronous reactive programming in Objective Caml
- Lucid Synchrone: experimental language for the implementation of reactive systems
Data Centric Languages
- CDuce: an XML-oriented functional language
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
- Coccinelle: a Coq library for term rewriting systems
- ALEA: a Coq library for reasoning on randomized algorithms
- PFF: a Coq library on floating-point arithmetic
- 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.
provides a Coq tactic for automatically proving some inequalities between
real-valued expressions containing elementary functions.