As announced in a previous post, I joined OCamlPro at the beginning of September and I started working on AltErgo. Here is a report presenting the tool and the work we have done during the two last months.
AltErgo at a Glance
AltErgo is an open source automatic theorem prover based on SMT technology. It is developed at Laboratoire de Recherche en Informatique, Inria Saclay IledeFrance and CNRS since 2006. It is capable of reasoning in a combination of several builtin theories such as uninterpreted equality, integer and rational arithmetic, arrays, records, enumerated data types and AC symbols. It also handles quantified formulas and has a polymorphic firstorder native input language. AltErgo is written in OCaml. Its core has been formally proved in the Coq proof assistant.
AltErgo has been involved in a qualification process (DO178C) by Airbus Industrie. During this process, a qualification kit has been produced. It was composed of a technical document with tool requirements (TR) that gives a precise description of each part of the prover, a companion document (~ 450 pages) of tests, and an instrumented version of the tool with a TR trace mechanism.
AltErgo Spider Web
AltErgo is mainly used to prove the validity of mathematical formulas generated by program verification platforms. It was originally designed and tuned to prove formulas generated by the Why tool. Now, it is used by different tools and in various contexts, in particular via the Why3 platform. As shown by the diagram below, AltErgo is used to prove formulas:
 generated from Ada code by SPARK 2005 and SPARK 2014,
 generated from C programs by FramaC and CAVEAT,
 produced from WhyML programs by Why3,
 translated from proof obligations generated by AtelierB,
Moreover, AltErgo is used in the context of cryptographic protocols verification by EasyCrypt and in SMTbased model checking by Cubicle.
Some “Hello World” Examples
Below are some basic formulas written in the why input syntax. Each example is proved valid by AltErgo. The first formulas is very simple and is proved with a straightforward arithmetic reasoning. "goal g2"
requires reasoning in the combination of functional arrays and linear arithmetic, etc. The last example contains a quantified subformula with a polymorphic variable x
. Generating four ground instances of this axiom where x
is replaced by 1
, true
, 1.4
and a
respectively is necessary to prove "goal g5"
.
[code language=”fsharp” title=”(*** Simple arithmetic formula ***)”]
goal g1 : 1 + 2 = 3
[/code]
[code language=”fsharp” title=”(*** Theories of functional arrays and linear integer arithmetic ***)”]
logic a : (int, int) farray
goal g2 : forall i:int. i = 6 > a[i<4][5] = a[i1]
[/code]
[code language=”fsharp” title=”(*** Theories of records and linear integer arithmetic ***)”]
type my_record = { a : int ; b : int }
goal g3 : forall v,w : my_record. 2 * v.a = 10 > { v with b = 5} = w > w.a = 5
[/code]
[code language=”fsharp” title=”(*** Theories of enumerated data types and uninterpreted equality ***)”]
type my_sum = A  B  C
logic P : ‘a > prop
goal g4 : forall x : my_sum. P(C) > x<>A and x<>B > P(x)
[/code]
[code language=”fsharp” title=”(*** Formula with quantifiers and polymorphism ***)”]
axiom a: forall x : ‘a. P(x)
goal g5 : P(1) and P(true) and P(1.4) and P(a)
[/code]
[code language=”bash” gutter=”false” title=”(*** formula with quantifiers and polymorphism ***)”]
$$ altergo examples.why
File “examples.why”, line 2, characters 121:Valid (0.0120) (0)
File “examples.why”, line 6, characters 153:Valid (0.0000) (1)
File “examples.why”, line 10, characters 181:Valid (0.0000) (3)
File “examples.why”, line 15, characters 159:Valid (0.0000) (6)
File “examples.why”, line 19, characters 147:Valid (0.0000) (10)
[/code]
AltErgo @ OCamlPro
On September 20, we officially announced the distribution and the support of AltErgo by OCamlPro and launched its new website. This site allows to download public releases of the prover and to discover available support offerings. It’ll be enriched with additional content progressively. The former AltErgo’s web page hosted by LRI is now devoted to theoretical foundations and academic aspects of the solver.
We have also published a new public release (version 0.95.2) of AltErgo. The main changes in this minor release are: source code reorganization into subdirectories, simplification of quantifiers instantiation heuristics, GUI improvement to reduce latency when opening large files, as well as various bug fixes.
In addition to the reimplementation and the simplification of some parts of the prover (e.g. internal literals representation, theories combination architecture, …), the main novelties of the current master branch of AltErgo are the following:
 The user can now specify an external (plugin) SATsolver instead of the default DFSbased engine. We experimentally provide a CDCL solver based on miniSAT that can be plugged to perform satisfiability reasoning. This solver is more efficient when formulas contain a rich propositional structure.
 We started the development of a new tool, called CtrlAltErgo, in which we put our expertise by implementing the most interesting strategies of AltErgo. The experiments we made with our internal benchmarks are very promising, as shown below.
Experimental Evaluation
We compared the performances of latest public releases of AltErgo with the current master branch of both AltErgo and CtrlAltErgo (commit ce0bba61a1fd234b85715ea2c96078121c913602
) on our internal test suite composed of 16209 formulas. Timeout was set to 60 seconds and memory was limited to 2GB per formula. Benchmarks descriptions and the results of our evaluation are given below.
Why3 Benchmark
This benchmark contains 2470 formulas generated from Why3’s gallery of WhyML programs. Some of these formulas are out of scope of current SMT solvers. For instance, the proof of some of them requires inductive reasoning.
SPARK Hilite Benchmark
This benchmark is composed of 3167 formulas generated from Ada programs used during Hilite project. It is known that some formulas are not valid.
BWare Benchmark
This testsuite contains 10572 formulas translated from proof obligations generated by AtelierB. These proof obligations are issued from industrial B projects and are proved valid.
AltErgo version 0.95.1 
AltErgo version 0.95.2 
AltErgo master branch* 
CtrlAltErgo master branch* 


Release date  Mar. 05, 2013  Sep. 20, 2013  – – –  – – – 
Why3 benchmark  2270 (91.90 %) 
2288 (92.63 %) 
2308 (93.44 %) 
2363 (95.67 %) 
SPARK benchmark  2351 (74.23 %) 
2360 (74.52 %) 
2373 (74.93 %) 
2404 (75.91 %) 
BWare benchmark  5609 (53.05 %) 
9437 (89.26 %) 
10072 (95.27 %) 
10373 (98.12 %) 
(*) commit ce0bba61a1fd234b85715ea2c96078121c913602