Software

Program Verification

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

Alt-Ergo: automatic prover modulo theories
CiME: term rewriting toolbox
Cubicle: a Parallel SMT-based model checker for parameterized systems
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

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.
Coq.Interval provides a Coq tactic for automatically proving some inequalities between real-valued expressions containing elementary functions.