Software

  • 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.
  • Isabelle (collaborative effort)
    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.
  • 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.
  • 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.