Release of Alt-Ergo 1.30 with experimental support for models generation
We have recently released a new (public up-to-date) version of Alt-Ergo. 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 Alt-Ergo 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 Alt-Ergo'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)
Models generation in Alt-Ergo is non-intrusive. It is controlled via a new option called
-interpretation. This option requires an integer argument. The default value
0 disables the feature, and:
-interpretation 1triggers a model computation and display at the end of Alt-Ergo's execution (i.e. just before returning
I don't know),
-interpretation 2triggers a model computation before each axioms instantiation round,
-interpretation 3is 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 Alt-Ergo timeouts, the latest computed model, if any, will be shown.
If you are not on Windows, you will also be able to use option
-interpretation-timelimit to try to get a candidate model even when Alt-Ergo hits a given time limit (set with option
-timelimit). The idea is simple: if Alt-Ergo 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, Alt-Ergo 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 non-constrained array
arrwill probably be uninterpreted in the model (which would mean that it can have any well-typed value at any well-typed index).
Model generation may not terminate in presence of non-linear arithmetic. This is actually the case for the example below (Alt-Ergo handles rationals, and there is no rational
x * x = 2). We plan to implement a
delta-completenesslike 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 Alt-Ergo, some ground terms may be missing. Moreover, no filtering with labels mechanism is done for the moment.
Alt-Ergo 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.
|Alt-Ergo 1.01||Alt-Ergo 1.20||Alt-Ergo 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 Alt-Ergo 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 Alt-Ergo's issues tracker on Github.
Don't hesitate to give your feedback to help us improving Alt-Ergo. You can also contribute with benchmarks to diversify and enrich our internal test-suite.
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 Why playform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.
Alt-Ergo is part of the formal method team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club