Abstract
In this talk, we present the design and use cases of the Alt-Ergo automatic demonstrator.
Alt-Ergo is a demonstrator from the SMT family specially designed to prove the validity of logic formulas generated by program verification tools such as Frama-C, Why3, Spark or Atelier-B. These formulas all share the same format: they contain data type declarations, axioms for defining complex data structures, memory models, specific theories (e.g. finite sets, floats, bit vectors) and finally proof obligations from program properties to be verified.
Alt-Ergo's design and implementation choices have all been guided by the need to deal efficiently with these kinds of formulas. Alt-Ergo is the only SMT demonstrator to directly handle formulas written in first-order logic with polymorphic types "à la ML". It also features predefined theories useful for proving programs, such as equality theory with non-interpreted symbols, arithmetic on integers and reals, polymorphic functional array theory with extensionality, enumerated types, records and associative/commutative (AC) symbols.
For processing formulas with quantifiers, Alt-Ergo relies on an original SAT-solver coupled with a "lazy" CNF technique, as well as an extended filtering algorithm for handling polymorphic terms. Its kernel also implements a unique decision procedure combination method based on rewriting techniques that enable it, for example, to handle associative/commutative symbols efficiently.
