Alt-Ergo Overview
In this preliminary chapter, we’ll have a look at Alt-Ergo. What is it ? What is it good for ? How does it interact with other tools ?
What is it ?
Automatic theorem prover
Alt-Ergo is an automatic theorem prover (ATP), specially designed to prove properties about programs, such as their correctness.
Unlike interactive theorem provers (ITP) – such as Coq, Agda, Isabelle and HOL – Alt-Ergo proves formulas by itself. Just Ask Alt-Ergo !
ATP are great at solving relatively simple problems, but some may still require human assistance. Tools such as Why3 make it possible to use ATP along with ITP.
A native language designed for program verification
Alt-Ergo’s native language is especially convenient for reasoning about computer programs.
Polymorphism and algebraic datatypes makes it easy to model various data structures.
It is human-readable, unlike most other languages for SMT-solvers.
Note that Alt-Ergo supports other input languages, such as SMT-LIB, the standard input language for SMT-solvers.
SMT-solver
More specifically, Alt-Ergo is an SMT-solver. Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing.
The Satisfiability Modulo Theory (SMT) problem is a decision problem.
SMT decision problem
- Input
A formula in first order logic
A theory: additional axioms which provide an interpretation for some symbols
- Output
Is the formula satisfiable (SAT) or unsatisfiable (UNSAT) ?
In other words, is it possible to find an interpretation of all symbols that makes the formula true while being compatible with the theory ?
As Alt-Ergo is specialized in theorems about programs, it actually states the problem in a slightly different way.
SMT decision problem in Alt-Ergo
- Input
A formula in first order logic
A theory: additional axioms which provide an interpretation for some symbols
- Output
Is the formula Valid or Invalid ?
In other words, is the formula true for all theory-compatible interpretations of the symbols ?
Note
Those two problems are actually the same: you can switch from one to the other by negating the formula !
A couple of things should be noted to give a better understanding of the problem.
Warning
Undecidability
This general version of the SMT problem is undecidable: it is impossible to write a program that will always answer Valid or Invalid in a finite time, and always give the correct answer !
Principle of explosion
If incompatible assumptions are made in the theory, no interpretation will be compatible with the theory. Therefore, all formulas will be Valid !
Because of this, Alt-Ergo can have other answers than Valid and Invalid.
Answer |
Meaning |
|---|---|
Valid |
The formula has been proven correct: all interpretations compatible with the axioms make the formula true. |
I don’t know |
The formula may or may not be valid. |
Inconsistent assumption |
An inconsistency has been detected in the theory ! |
Invalid |
There exists an interpretation which falsifies the formula. |
Note that as Alt-Ergo focuses on proving that programs are correct, the last case doesn’t currently happen: Alt-Ergo will answer I don’t know rather than Invalid.
In other words, Alt-Ergo deals with UNSAT, not SAT.
Some experimental support exists for the generation of counter-examples (models) which falsifies the formula. This will be expanded in future versions.
Reasoners for several theories
Note that this undecidability depends on the axioms being used. For several interesting theories, the problem is actually decidable.
Alt-Ergo has built-in support for a number of interesting theories, relevant to computer programs.
The free theory of equality with uninterpreted symbols
Associative and commutative (AC) symbols
Linear arithmetic over integers and rationals
(Fragment of) non-linear arithmetic
Floating-point arithmetic (as an extension)
Enumerated datatypes
Record datatypes
Polymorphic functional arrays
Fixed-size bitvectors
Creating reasoners for a combination of theories is a difficult problem, even when a reasoner is known for each of these theories taken separately.
Alt-Ergo handles this issue through a combination of Shostak-like and Nelson-Oppen like approaches.
Thanks to this, Alt-Ergo is great at reasoning on real-life problems, which often mix several theories.
How does it relate to other tools ?
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 platform. Currently, it is used as a back-end of different tools and in various settings, in particular via the Why3 platform. For instance, the Frama-C suite relies on it to prove formulas generated from C code, and the SPARK toolset uses it to check formulas produced from Ada programs. In addition, Alt-Ergo is used to prove formulas issued from B modelizations and from cryptographic protocols verification. The figure given below shows the main tools that rely on Alt-Ergo to prove the formulas they generate.
