Release of Alt-Ergo 2.4.0

Authors: Albin Coquereau
Date: 2021-01-22
Category: Formal Methods
Tags: alt-ergo


A new release of Alt-Ergo (version 2.4.0) is available.

You can get it from Alt-Ergo's website. The associated opam package will be published in the next few days.

This release contains some major novelties:

  • Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard.
  • We switched command line parsing to use cmdliner. You will need to use --<option name> instead of -<option name>. Some options have also been renamed, see the manpage or the documentation.
  • We improved the online documentation of your solver, available here.

This release also contains some minor novelties:

  • .mlw and .why extension are depreciated, the use of .ae extension is advised.
  • Add --input (resp --output) option to manually set the input (resp output) file format
  • Add --pretty-output option to add better debug formatting and to add colors
  • Add exponentiation operation, ** in native Alt-Ergo syntax. The operator is fully interpreted when applied to constants
  • Fix --steps-count and improve the way steps are counted (AdaCore contribution)
  • Add --instantiation-heuristic option that can enable lighter or heavier instantiation
  • Reduce the instantiation context (considered foralls / exists) in CDCL-Tableaux to better mimic the Tableaux-like SAT solver
  • Multiple bugfixes

The full list of changes is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!


About Alt-Ergo

Alt-Ergo is an Open Source automatic solver of mathematical formulas designed for program verification. Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.