
AltErgo is an opensource automatic solver of mathematical formulas
designed for program verification. It is based on Satisfiability
Modulo Theories (SMT).

ℂDuce is a modern XMLoriented functional language with
innovative features. A compiler is available under the terms of an
opensource license. ℂDuce is typesafe, efficient, and offers
powerful constructions to work with XML documents.

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.

The Coq.Interval library provides vernacular files containing tactics for
simplifying the proofs of inequalities on expressions of real numbers
for the Coq proof assistant.

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.

Cubicle is an open source model checker for verifying safety
properties of arraybased systems, which corresponds to a syntacticallyrestricted
class of parametrized transition systems with states represented as
arrays indexed with an arbitrary number of processes. Cache coherence
protocols and mutual exclusion algorithms are typical examples of such
systems.

Flocq (Floats for Coq)
is a formalization of floatingpoint arithmetic for the Coq system.
It provides a comprehensive library of theorems on a multiradix
multiprecision arithmetic; it also supports efficient numerical
computations inside Coq.

Gappa is a tool intended to help verifying and formally proving properties on
numerical programs dealing with floatingpoint or fixedpoint arithmetic.

HOLTestGen is a is a test case generator for specification based testing.
HOLTestGen is built on top of the specification and theorem proving environment
Isabelle/HOL. HOLTestGen allows one to write test specifications in
HOL and (semi)automatically partition the input space; using a
foreign language interface, implementations in arbitrary languages can be tested.

Krakatoa and Jessie are frontends of
Why3, for deductive verification of behavioral properties of Java and C programs.

The
Isabelle System
is one of the major existing interactive theorem proving systems of the world;
the group substantially contributed to its evolution of parallized evaluation
mechanisms both in the inference engine as well on the level of advanced
IDElike interfaces.

PFF is a Coq
formalization of floatingpoint arithmetic with highlevel
definitions and highlevel properties. It is now subsumed by the
Flocq library.

Rukia is a C++ library to explore graphical models by generating at random paths
in automata. Instead of using an isotropic random walk (i.e., choosing the next
state uniformly at random among the successors of the current state), Rukia
guides the random walk to guarantee a global uniform distribution among the
elements to be covered, whatever the model topology.

Schora is a tool (with an online version) to deal with Symbolic Choreography analysis. It allows to check if a set of peers conforms to the choreography. It allows also to check if a choreography is realizable.

SWST is a Symbolic Web Service Composition Testing tool. It is an
endtoend chain for testing service compositions from BPEL
specification to java implementation of the composition.

A platform for deductive program verification.