Release of AltErgo 1.30 with experimental support for models generation
We have recently released a new (public uptodate) version of AltErgo. We focus in this article on its main new feature: experimental support for models generation. This work has been done with Frédéric Lang, an intern at OCamlPro from February to July 2016.
The idea behind models generation
The idea behind this feature is the following: when AltErgo fails to prove the validity of a given formula F
, it tries to compute and exhibit values for the terms of the problem that make the negation of F
satisfiable. For instance, for the following example, written in AltErgo's syntax,
logic f : int > int
logic a, b : int
goal g:
(a <> b and f(a) <= f(b) + 2*a) >
false
a possible (counter) model is a = 1
, b = 3
, f(a) = 0
, and f(b) = 0
. The solution is called a candidate
model because universally quantified formulas are, in general, not taken into account. We talk about counter example
or counter model
because the solution falsifies (i.e. satisfies the negation of) F
.
Basic usage
Models generation in AltErgo is nonintrusive. It is controlled via a new option called interpretation
. This option requires an integer argument. The default value 0
disables the feature, and:
interpretation 1
triggers a model computation and display at the end of AltErgo's execution (i.e. just before returningI don't know
),interpretation 2
triggers a model computation before each axioms instantiation round,interpretation 3
is the most aggressive. It triggers a model computation before each Boolean decision in the SAT.
For the two latest strategies, the model will be displayed at the end of the execution if the given formula is not proved. Note that a negative argument (1, 2, or 3) will enable model computation as explained above, but the result will not be displayed (useful for automatic testing). In addition, if AltErgo timeouts, the latest computed model, if any, will be shown.
Advanced usage
If you are not on Windows, you will also be able to use option interpretationtimelimit
to try to get a candidate model even when AltErgo hits a given time limit (set with option timelimit
). The idea is simple: if AltErgo fails to prove validity during the time allocated for "proof search", it will activate models generation and tries to get a counter example during the time allocated for that.
Form of produced models
Currently, models are printed in a syntax similar to SMT2's. We made this choice because Why3 already parses models in this format. For instance, AltErgo outputs the following model for the example above:
(
(a 1)
(b 3)
((f 3) 0)
((f 1) 0)
)
Some known issues and limitations

For the moment, arrays are interpreted in term of the accesses that appear in the input formula, or that have been added internally by the decision procedure. In particular, a nonconstrained array
arr
will probably be uninterpreted in the model (which would mean that it can have any welltyped value at any welltyped index). 
Model generation may not terminate in presence of nonlinear arithmetic. This is actually the case for the example below (AltErgo handles rationals, and there is no rational
x
such thatx * x = 2
). We plan to implement adeltacompleteness
like approach to stop splitting when intervals become really too small.goal g: forall x : real. x * x = 2. > false
. 
Currently, we generate a model for the content of the decision procedures part. Since the SAT's model is (in general) partial in AltErgo, some ground terms may be missing. Moreover, no filtering with labels mechanism is done for the moment.
AltErgo 1.30 vs 1.20 vs 1.01 releases
A quick comparison between this new version, the latest private release (1.20), and the latest public release (1.01) on our internal benchmarks is shown below. You notice that this version is faster and discharges more formulas.
AltErgo 1.01  AltErgo 1.20  AltErgo 1.30  
Why3 benchmarks (9752 VCs)  88.36% 7310 seconds  89.23% 7155 seconds  89.57% 4553 seconds 
SPARK benchmarks (14442 VCs)  78.05% 3872 seconds  78.42% 3042 seconds  78.56% 2909 seconds 
BWare benchmarks (12828 VCs)  97.38% 6373 seconds  98.02% 6907 seconds  98.31% 4231 seconds 
Download, install and bugs report
You can learn more about AltErgo and download the latest version on the solver's website. You can also install it via the OPAM package manager. For bugs report, we recommend AltErgo's issues tracker on Github.
Don't hesitate to give your feedback to help us improving AltErgo. You can also contribute with benchmarks to diversify and enrich our internal testsuite.
About AltErgo
AltErgo is an Open Source automatic solver of mathematical formulas designed for program verification. AltErgo 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é ParisSaclay 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 AltErgo Users' Club members. If AltErgo has been valuable to you, consider joining the AltErgo Users' Club.
Most Recent Articles
2024
 Archéologie de la Généalogie: prise en main et optimisation d’un logiciel vieux de 30 ans
 AltErgo 2.6 is Out!
 Flambda2 Ep. 3: Speculative Inlining
 opam 2.2.0 release!
 Flambda2 Ep. 2: Loopifying TailRecursive Functions
 Fixing and Optimizing the GnuCOBOL Preprocessor
 OCaml Backtraces on Uncaught Exceptions
 Opam 102: Pinning Packages
 Flambda2 Ep. 1: Foundational Design Decisions
 Behind the Scenes of the OCaml Optimising Compiler Flambda2: Introduction and Roadmap
 Lean 4: When Sound Programs become a Choice
 Opam 101: The First Steps
2023
 Maturing LearnOCaml to version 1.0: Gateway to the OCaml World
 The latest release of AltErgo version 2.5.1 is out, with improved SMTLIB and bitvector support!
 2022 at OCamlPro
 Autofonce, GNU Autotests Revisited
 Subsingleinstruction Peano to machine integer conversion
 Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
 Release of ocplibsimplex, version 0.5
 The Growth of the OCaml Distribution