Welcome to Try-Alt-Ergo!

Try-Alt-Ergo is a JavaScript-based version of Alt-Ergo that can be run on compatible browsers (eg. Firefox, Chromium) without requiring a server for computations.

What is Alt-Ergo?

Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. It is based on Satisfiability Modulo Theories (SMT).

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, especially 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.

Its language

Alt-Ergo's native input language is a polymorphic first-order logic "à la ML" modulo theories. This logic is very suitable for expressing formulas generated in the context of program verification. Currently, Alt-Ergo is capable of reasoning in the combination of the following built-in theories:

  • the free theory of equality with uninterpreted symbols,
  • linear arithmetic over integers and rationals,
  • fragments of non-linear arithmetic,
  • polymorphic functional arrays with extensionality,
  • enumerated datatypes,
  • record datatypes,
  • associative and commutative (AC) symbols,
  • fixed-size bit-vectors with concatenation and extraction operators.

How to use Try-Alt-Ergo?

  • Click on the Ask Alt-Ergo button at the top left of the page
  • A message should appear at the bottom left of the page
  • This message contains the answer of AE for the small example in the editor
  • To learn more about the Alt-Ergo's syntax, click on the Documentation button at the top of the page
  • Click on the tutorial button if you want an introduction to Alt-Ergo and its native language.
  • You can edit the example or click on the Load button at the top right of the page to load another example, or a file from your computer
  • The save button allows you to export the file you wrote from the editor
  • You can change some options like the time limit or the input format if you want to write a file in Smt-Lib2 format in the options tab

Alt-Ergo outputs

This page aims to output all the messages returned by Alt-Ergo. On this page, you will find more information than in the output console, such as debug informations (if set).


Status

Error and Warning

Model / Unsat Core

Debug informations

Alt-Ergo options

On this page, you will find some options for the Alt-Ergo execution. These options are divided into three parts:
  • The first part contains the most commonly used options of Alt-Ergo such as the time limit or the input file format.
  • The second section contains the more advanced options of Alt-Ergo.
  • The last part contains the debugging flag allowing the user to have more information about specific modules or reasoners in Alt-Ergo

Name of the file, used in messages and names the saved file

Limit

Set the time limit in seconds
Set the limit of steps to reach before Alt-Ergo stops. -1 (default) = no steps limit setted

Format


Set the input format of the file to solve
Native to solve file in the native Alt-Ergo format
Smt-lib2 to solve file in the SMT standard format

Native outputs Valid/Invalid/I don't know
Smt-lib2 outputs unsat/sat/unknown

Output generation

Experimental support for counter-example generation. Do not work in case of timeout
None: do not compute any interpretation
Last: compute an interpretation before returning unknown
Every: compute an interpretation before every instantiation phase and returns the last interpretation computed
Unsat Core

Internal


Normal (default), only do light instantiation phases
Auto, try some light instantiation phases, if no new instances are made it tries some heavier heuristic
Greedy use all available ground terms in instantiation

Tableaux solver (default) is the functional SAT solver of Alt-Ergo, specially tuned for program verification. This solver is the only one compatible with model, interpretation and unsat-core generation
CDLC solver is an imperative SAT solver. It offers good performance on heavy boolean problems
CDCL-Tableaux solver is based on the CDCL SAT solver with an optimisation that improves overall performances

Case-split


Set the case-split policy to use
Maximum size of case-split
Enable Adts case-split

Sat

Tableaux
No learning in sat
No backward
No backjumping
No decisions
Disable decisions at the SAT level for the instances generated from the given axioms
Bottom classes
CDCL
Enable restarts
No tableau in instantiations
No tableau in theory
No flat formulas simplification
No Minimal Bj

Instantiation

Set the age limit bound
Instantiate after Bj
Normalize instances
No e-matching
No arith matching
Triggers
Maximum number of triggers used (including regular and multi triggers)
Maximum size of multi-triggers, i.e. the maximum number of independent patterns in a multi-trigger
Triggers variable
No user triggers

Theory

Restricted
No tcp
No theory
No Adts
No AC
No contragru
No ite
Inline lets
Rewriting
Arithmetic
Tighten vars
Skip Fourier-Motzkin variables elimination steps that may produce a number of inequalities that is greater than the given limit. However, unit eliminations are always done
No FM
No NLA

Verbose flag
Debug
AC
Adt
Arith
Arrays
Bitv
CC
Combine
Constr
Explanations
Fm
GC
Interpretation
Ite

Set the debugging flag of E-matching
Sat
Split
Sum
Triggers
Types
Typing
Uf
Unsat Core
Use
Warnings

Outputs used rules

Execution statistics

This section is still Work In Progress
At this time it only outputs the usage of axioms in instances

Instantiated quantified axioms and predicates

Examples

Default


type 'a set

logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop

axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <-> (x = y or mem(x, s))

logic is1, is2 : int set
logic iss : int set set

goal g:
is1 = is2 ->
mem (is1, add (is2, iss))

Linear Arithmetic


goal g_1 :
forall x,y,z,t:int.
0 <= y + z <= 1 ->
x + t + y + z = 1 ->
y + z <> 0 ->
x + t = 0

Uninterpreted functions and Arithmetic


logic h,g,f: int,int -> int
logic a, b:int

goal g_2 :
h(g(a,a),g(b,b)) = g(b,b) ->
a = b ->
g(f(h(g(a,a),g(b,b)),b) - f(g(b,b),a),
f(h(g(a,a),g(b,b)),a) - f(g(b,b),b))
= g(0,0)

Quantifiers


type 'a pointer
type 'a pset

logic P : int -> prop
logic Q : int , int -> prop

axiom a:
(forall x:int.
(P(x) <->
(exists i:int. exists r: int.
Q(r,i)
)
)
)

goal g_3 :
Q(1,2) -> P(4)

Polymorphism


type 'a set

logic empty : 'a set
logic add : 'a , 'a set -> 'a set
logic mem : 'a , 'a set -> prop

axiom mem_empty:
forall x : 'a.
not mem(x, empty : 'a set)

axiom mem_add:
forall x, y : 'a. forall s : 'a set.
mem(x, add(y, s)) <-> (x = y or mem(x, s))

logic is1, is2 : int set
logic iss : int set set

goal g_4:
is1 = is2 ->
(not mem(1, add(2+3, empty : int set))) and
mem (is1, add (is2, iss))

Arrays


goal g_5 :
forall i,j,k:int.
forall v,w : 'a.
forall b : 'a farray.
b = b[j<-b[i],k<-w] ->
i = 1 ->
j = 2 ->
k = 1 ->
b[i] = b[j]

Enumerations and Arrays


type t = A | B | C | D
type t2 = E | F | G | H

goal g_6 :
forall a : (t,t2) farray.
a[B <- E][A] <> E ->
a[C <- F][A] <> F ->
a[D <- G][A] <> G ->
a[A] = H

Non-linear Arithmetic


goal g_7 :
forall x,y,z:int.
x > 3 ->
y > 0 ->
z > 0 ->
y > z ->
z = ((x / y) + y) / 2 ->
z > 1 and y > 2

About Try-Alt-Ergo

Try-Alt-Ergo is a work fully funded by OCamlPro, and maintained by the Alt-Ergo development team

This website uses the Alt-Ergo's web worker obtained by compiling the bytecode executable of the solver into JavaScript thanks to Js_of_ocaml. The web worker uses json file to receive input file as long as options and to send answers. This allows the web worker to be run directly in Js code such as in the Try-Alt-Ergo tutorial. We use the Data-encoding library to convert our data to json throught OCaml code. Alt-Ergo also needs Zarith stubs js to be compiled in Js.

Try-Alt-Ergo uses the Lwt library to run the Alt-Ergo web worker. It uses a combination of Tyxml, Bootstrap and the Ace code editor to produce the resulting website.