As announced in [a previous post](/blog/2013_09_04_ocamlpro_highlights_august_2013), I joined OCamlPro at the beginning of September and I started working on Alt-Ergo. Here is a report presenting the tool and the work we have done during the two last months.

### Alt-Ergo at a Glance

[Alt-Ergo](https://alt-ergo.ocamlpro.com) is an open source automatic theorem prover based on [SMT](https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories) technology. It is developed at [Laboratoire de Recherche en Informatique](https://www.lri.fr), [Inria Saclay Ile-de-France](https://www.inria.fr/centre/saclay) and [CNRS](https://www.cnrs.fr/index.php) since 2006. It is capable of reasoning in a combination of several built-in 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 first-order native input language. Alt-Ergo is written in [OCaml](https://caml.inria.fr/ocaml/index.fr.html). Its core has been formally proved in the [Coq proof assistant](https://coq.inria.fr).

Alt-Ergo has been involved in a qualification process (DO-178C) by [Airbus Industrie](http://www.airbus.com). 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.

### Alt-Ergo Spider Web

Alt-Ergo 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](https://why.lri.fr). Now, it is used by different tools and in various contexts, in particular via the [Why3 platform](https://why3.lri.fr). As shown by the diagram below, Alt-Ergo is used to prove formulas:

- generated from Ada code by SPARK 2005 and [SPARK 2014](https://www.spark-2014.org),

- generated from C programs by [Frama-C](https://frama-c.com) and [CAVEAT](https://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=1028953&tag=1),

- produced from WhyML programs by [Why3](https://why3.lri.fr),

- translated from proof obligations generated by [Atelier-B](https://www.atelierb.eu),

Moreover, Alt-Ergo is used in the context of cryptographic protocols verification by [EasyCrypt](https://www.easycrypt.info) and in SMT-based model checking by [Cubicle](https://cubicle.lri.fr).

Below are some basic formulas written in the why input syntax. Each example is proved valid by Alt-Ergo. 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 sub-formula 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``.

** Simple arithmetic operation **

```ocaml

goalg1:1+2=3

```

** Theories of functional arrays and linear integer arithmetic **

```ocaml

logica:(int,int)farray

goalg2:foralli:int.i=6->a[i<-4][5]=a[i-1]

```

** Theories of records and linear integer arithmetic **

** Theories of enumerated data types and uninterpreted equality **

```ocaml

typemy_sum=A|B|C

logicP:'a->prop

goalg4:forallx:my_sum.P(C)->x<>Aandx<>B->P(x)

```

** Formula with quantifiers and polymorphism **

```ocaml

axioma:forallx:'a.P(x)

goalg5:P(1)andP(true)andP(1.4)andP(a)

```

** formula with quantifiers and polymorphism **

```shell-session

$$ alt-ergo examples.why

File "examples.why", line 2, characters 1-21:Valid (0.0120) (0)

File "examples.why", line 6, characters 1-53:Valid (0.0000) (1)

File "examples.why", line 10, characters 1-81:Valid (0.0000) (3)

File "examples.why", line 15, characters 1-59:Valid (0.0000) (6)

File "examples.why", line 19, characters 1-47:Valid (0.0000) (10)

```

### Alt-Ergo @ OCamlPro

On September 20, we officially announced the distribution and the support of Alt-Ergo by OCamlPro and launched its [new website](https://alt-ergo.ocamlpro.com). 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 Alt-Ergo'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 Alt-Ergo. The main changes in this minor release are: source code reorganization into sub-directories, simplification of quantifiers instantiation heuristics, GUI improvement to reduce latency when opening large files, as well as various bug fixes.

In addition to the re-implementation 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 Alt-Ergo are the following:

- The user can now specify an external (plug-in) SAT-solver instead of the default DFS-based 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 Ctrl-Alt-Ergo, in which we put our expertise by implementing the most interesting strategies of Alt-Ergo. 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 Alt-Ergo with the current master branch of both Alt-Ergo and Ctrl-Alt-Ergo (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 Hi-lite Benchmark

This benchmark is composed of 3167 formulas generated from Ada programs used during Hi-lite project. It is known that some formulas are not valid.

#### BWare Benchmark

This test-suite contains 10572 formulas translated from proof obligations generated by Atelier-B. These proof obligations are issued from industrial B projects and are proved valid.