Overview
AltErgo is an opensource SMT solver dedicated to the proof of mathematical formulas generated in the context of program verification. It is built upon CC(X): a congruence closure algorithm parametrized by a Shostak theory X. Currently, AltErgo provides a builtin support for the following theories:
 the free theory of equality with uninterpreted symbols,
 linear arithmetic over integers and rationals,
 nonlinear arithmetic,
 polymorphic functional arrays,
 enumerated datatypes,
 record datatypes,
 associative and commutative (AC) symbols,
 fixedsize bitvectors.
AltErgo is highly parametrized and modular. Each component is described by a set of inference rules and is implemented as an OCaml (parametrized) module. Its native input language is a polymorphic firstorder logic modulo theories. It also provides a partial support for the SMTLIB (v1.2 and v2) standard inputs. Since September 2013, AltErgo is maintained and distributed by the OCamlPro company, while academic research is conducted in partnership with the VALS/Toccata teams (LRI).
Research Projects Involving AltErgo
 BWare (2013  2016)
 Cafein (2013  2016)
 FUI HiLite (2010  2013)
 Decert (2009  2012)
 ADT AltErgo (2009  2011)
 A3PAT (2005  2009)
Related Publications
Arithmetic

A Collaborative Framework for NonLinear Integer Arithmetic Reasoning in AltErgo.
Sylvain Conchon, Mohamed Iguernelala and Alain Mebsout. SYNASC, 2013 (to appear). 
A Simplexbased extension of FourierMotzkin for solving linear integer arithmetic.
François Bobot, Sylvain Conchon, Evelyne Contejean, Mohamed Iguernelala, Assia Mahboubi, Alain Mebsout, and Guillaume Melquiond. IJCAR, 2012. [bib] 
Builtin treatment of an axiomatic floatingpoint theory for SMT solvers.
Sylvain Conchon, Guillaume Melquiond, Cody Roux, and Mohamed Iguernelala. SMT, 2012. [bib]
Shostaklike theories combination

Canonized rewriting and ground AC completion modulo Shostak theories: Design and implementation.
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. LMCS, 2012. [bib] 
Canonized Rewriting and Ground AC Completion Modulo Shostak Theories.
Sylvain Conchon, Évelyne Contejean, and Mohamed Iguernelala. TACAS, 2011. [bib] 
CC(X): Semantical combination of congruence closure with solvable theories.
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. ENTCS, 2007. [bib] 
CC(X): Efficiently combining equality and solvable theories without canonizers.
Sylvain Conchon, Évelyne Contejean, and Johannes Kanig. SMT Workshop, 2007. [bib]
Quantifiers

Reasoning with triggers.
Claire Dross, Sylvain Conchon, Johannes Kanig, and Andrei Paskevich. SMT workshop, 2012. [bib] 
Implementing Polymorphism in SMT solvers.
François Bobot, Sylvain Conchon, Évelyne Contejean, and Stéphane Lescuyer. SMT Workshop, 2008. [bib]
Certification

Improving Coq propositional reasoning using a lazy CNF conversion scheme.
Stéphane Lescuyer and Sylvain Conchon. FroCoS, 2009. [bib] 
A reflexive formalization of a SAT solver in Coq.
Stéphane Lescuyer and Sylvain Conchon. TPHOLs, 2008. [bib] 
Lightweight Integration of the Ergo Theorem Prover inside a Proof Assistant.
Sylvain Conchon, Évelyne Contejean, Johannes Kanig, and Stéphane Lescuyer. AFM, 2007. [bib]
Theses

Strengthening the Heart of an SMTSolver: Design and Implementation of Efficient Decision Procedures.
Mohamed Iguernelala. PhD thesis, 2013. [bib] 
SMT Techniques and their Applications: from AltErgo to Cubicle.
Sylvain Conchon. Habilitation thesis, 2012. [bib] 
Formalizing and Implementing a Reflexive Tactic for Automated Deduction in Coq
Stéphane Lescuyer. PhD thesis, 2011. [bib]