-
Alt-Ergo is an open-source automatic solver of mathematical formulas
designed for program verification. It is based on Satisfiability
Modulo Theories (SMT).
-
ℂDuce is a modern XML-oriented functional language with
innovative features. A compiler is available under the terms of an
open-source license. ℂDuce is type-safe, 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 array-based systems, which corresponds to a syntactically-restricted
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 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.
-
Gappa is a tool intended to help verifying and formally proving properties on
numerical programs dealing with floating-point or fixed-point arithmetic.
-
HOL-TestGen is a is a test case generator for specification based testing.
HOL-TestGen is built on top of the specification and theorem proving environment
Isabelle/HOL. HOL-TestGen 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 front-ends of
Why3, for deductive verification of behavioral properties of Java and C programs.
-
Iris is a Higher-Order Concurrent Separation Logic Framework
implemented and verified in the proof assistant Coq. It can be used
for reasoning about safety of concurrent programs, as the logic in
logical relations, to reason about type systems, etc. Iris is
developed at VALS, jointly with MPI-SWS (Germany), the Delft University
of Technology (Pays-Bas) and with the Aarhus University (Denmark).
-
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
IDE-like interfaces.
-
Pactole is a Coq formal
framework for describing and reasoning about dynamic mobile sensor
networks, and in particular proving the correctness of localised
distributed protocols for such mobile sensor networks.
-
PFF is a Coq
formalization of floating-point arithmetic with high-level
definitions and high-level 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.
-
SMTCoq is a plugin for the Coq proof assistant that provides new decision procedures based on external automatic provers.
-
SWST is a Symbolic Web Service Composition Testing tool. It is an
end-to-end chain for testing service compositions from BPEL
specification to java implementation of the composition.
-
A platform for deductive program verification.