haRVey is a SMT (Satisfiability Modulo Theories) prover. There are presently two branches of haRVey: haRVey-SAT and haRVey-FOL.

• haRVey-FOL integrates a First-Order Logic theorem prover (hence its name), i.e. the E-prover. It uses the superposition calculus as implemented by the E-prover, to determine the satisfiability of Boolean combinations of atoms with functions interpreted in a first-order theory with equality.
  

• haRVey-SAT is based on congruence closure, the Nelson-Oppen framework, and rudimentary instantiation techniques to decide the satisfiability of a set of atoms written with uninterpreted symbols, linear arithmetics, some lambda-expressions, and some quantifiers. The Boolean engine is a SAT solver (zChaff or MiniSAT), hence its name.
  

• License:
  
  • haRVey-FOL: GNU LGPL 2.1
    
    • haRVey-FOL relies on E-prover (http://eprover.org/): GNU GPL
      
  • haRVey-SAT: BSD like
    
    • haRVey-SAT relies on MiniSat(http://minisat.se/): BSD like
      
• Web site: http://harvey.loria.fr/haRVey.php
  

Zenon is an automatic theorem that handles first-order logic with equality. Its most important feature is that it outputs the proofs of the theorems, in Coq-checkable form.

• License: BSD like
  
• Web site: http://focal.inria.fr/zenon/
  

CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT) problems. It can be used to prove the validity (or, dually, the satisfiability) of first-order formulas in a large number of built-in logical theories and their combination.

CVC3 is the last offspring of a series of popular SMT provers, which originated at Stanford University with the SVC system. In particular, it builds on the code base of CVC Lite, its most recent predecessor. Its high level design follows that of the Sammy prover.

CVC3 works with a version of first-order logic with polymorphic types and has a wide variety of features including:

• several built-in base theories: rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bit vectors, and equality over uninterpreted function symbols;
  
• support for quantifiers;
  
• an interactive text-based interface;
  
• a rich C and C++ API for embedding in other systems;
  
• proof and model generation abilities;
  
• predicate subtyping;
  
• essentially no limit on its use for research or commercial purposes (see license).
  

• License: BSD like
  
• Web site: http://www.cs.nyu.edu/acsys/cvc3/
  

The heart of SAL is a language, developed in collaboration with Stanford and Berkeley, for specifying concurrent systems in a compositional way. It is supported by a tool suite that includes state of the art symbolic (BDD-based) and bounded (SAT-based) model checkers, an experimental “Witness” model checker, and a unique “infinite” bounded model checker based on SMT solving. Auxiliary tools include a simulator, deadlock checker and an automated test generator.

• License: GNU GPL
  
• Web site: http://sal.csl.sri.com/
  

Alt-Ergo is an automatic theorem prover dedicated to program verification. Alt-Ergo is based on CC(X) a congruence closure algorithm parameterized by an equational theory X. Currently, CC(X) can be instantiated by the empty equational theory and by the linear arithmetics. Alt-Ergo contains also a home made SAT-solver and an instantiation mechanism.

• License: GNU GPL
  
• Web site: http://alt-ergo.lri.fr/
  

Gappa (Génération Automatique de Preuves de Propriétés Arithmétiques) is a tool intended to help verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic. It has been used to write robust floating-point filters for CGAL and it is used to certify elementary functions in CRlibm. While Gappa is intended to be used directly, it can also act as a backend prover for the Why software verification plateform or as an automatic tactic for the Coq proof assistant.

• License: GNU LGPL and CeCILL
• Web site: http://gappa.gforge.inria.fr/