Alt-Ergo is a \\\"little engine\\\" of proof dedicated to program verification, whose development started in 2006.
It solves goals that are directly written in the Why\\\'s annotation language; this means that Alt-Ergo fully supports first order polymorphic logic with quantifiers.
It also supports the SMT standard defined by the SMT-lib initiative.
