Ergo: a theorem prover for polymorphic first-order logic modulo theories

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 sym- bols and a built-in theory X. Its architecture is highly modular and it consists only of 3000 lines of Ocaml code. It is currently used to prove correctness of C and Java programs.