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.

Contents

• Install
  • From a package manager
  • From sources
• Usage
  • Library
  • Run
  • Javascript
• Input file formats
  • Alt-Ergo's native language
  • SMT-LIB 2
• API documentation
• Plugins
  • AB why3 plugins
• Developer's documentation
  • Project Architecture
  • Contributing guidelines
• About
  • Licenses
  • Changes
  • Try-Alt-Ergo
  • Alt-Ergo's website
  • Scientific publications