Welcome to Alt-Ergo’s documentation!

Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. It is based on Satisfiability Modulo Theories (SMT). Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing.

It was developed at LRI, and is now improved and maintained at OCamlPro, and friendly collaboration is maintained with the Why3 development team.

You can try Alt-Ergo online. You can also learn more about our partners with the Alt-Ergo Users’ Club.

If you are using Alt-Ergo as a library, see the API documentation (also available on ocaml.org).

Input file formats

Alt-ergo supports different input languages:

• Alt-ergo supports the SMT-LIB language v2.6. This is Alt-Ergo’s preferred and recommended input format.

• The original input language is its native language, based on the language of the Why3 platform. Since the version 2.6.0, this language is deprecated.

• It also (partially) supports the input language of Why3 through the AB-Why3 plugin.

Contents

• Install
  • From a package manager
  • From GitHub releases (Linux and macOS)
  • From sources
• Usage
  • Command-line
  • Library
  • Javascript
• SMT-LIB language
  • Bit-vectors
  • Floating-Point Arithmetic
• Alt-Ergo's native language
  • Summary
  • Declaration of symbols
  • Types
  • Declaration of axioms
  • Setting goals
  • Theories
  • Control Flow
  • Syntax of declarations and expressions
• Model generation
  • Activation
  • Correctness of model generation
  • Examples
• Optimization
  • MaxSMT syntax
  • Activation
  • Examples
• API documentation
• Plugins
  • Inequality plugins
  • AB why3 plugin (deprecated)
• Developer's documentation
  • Project Architecture
  • Contributing guidelines
• About
  • Licenses
  • Changes
  • Try-Alt-Ergo
  • Alt-Ergo's website
  • Scientific publications