## CC(X): Efficiently Combining Equality and Solvable Theories without Canonizers## Sylvain Conchon, Évelyne Contejean and Johannes Kanig |

Abstract: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.

This document was translated from L^{A}T_{E}X byH^{E}V^{E}A.