Ergo is a little engine of proof dedicated to program verification. It fully supports quantifiers and directly handles polymorphic sorts. Its core component is CC(X), a new combination scheme for the theory of uninterpreted symbols parameterized by a built-in theory X. In order to make a sound integration in a proof assistant possible, Ergo is capable of generating proof traces for CC(X). Alternatively, Ergo can also be called interactively as a simple oracle without further verification. It is currently used to prove correctness of C and Java programs as part of the Why platform.

Polymorphism has become a common way of designing short and reusable programs by abstracting generic definitions from type-specific ones. Such a convenience is valuable in logic as well, because it unburdens the specifier from writing redundant declarations of logical symbols. However, top shelf automated theorem provers (ATP), such as Simplify, Yices or other SMT-LIB ones do not handle polymorphism. To this end, we present efficient reductions of polymorphism in both unsorted and many-sorted first order logics. For each encoding, we show that the formulas and their encoded counterparts are logically equivalent in the context of automated theorem proving. The efficiency keynote is to disturb the prover as little as possible, especially the decision procedures used for special sorts, e.g. integer linear arithmetic, to which we apply a special treatment. The corresponding implementations are presented in the Why/Caduceus toolkit, used as a proof obligations generator.

Our goal is to be able to use automated provers to certify programs. Provers often work on monomorphic or untyped logics whereas certification involves more complicated logics. To this end, we present an encoding of multisorted polymorphic first-order logic to unsorted first-order logic where the typing information is encoded directly into terms. Unlike formulae translated with the more natural encoding based on typing predicates, formulae translated with our encoding can be dealt with efficiently by automated theorem provers. We show that translated formulae are logically equivalent to their typed original counterparts, and we describe an implementation of this encoding in the Why program certification tool. This implementation also illustrates the issue of dealing with provers that have built-in decision procedures, e.g. arithmetic in Simplify. We finally present the results we obtained on certifying a significant number of real C programs with Why and Simplify.