*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.

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.

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.

- 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

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).

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

Set the time limit in seconds

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

Set the input format of the file to solve

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

Set the case-split policy to use

Maximum size of case-split

Enable Adts case-split

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

Enable restarts

No tableau in instantiations

No tableau in theory

No flat formulas simplification

No Minimal Bj

Set the age limit bound

Instantiate after Bj

Normalize instances

No e-matching

No arith matching

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

Restricted

No tcp

No theory

No Adts

No AC

No contragru

No ite

Inline lets

Rewriting

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

This section is still Work In Progress

At this time it only outputs the usage of axioms in instances

`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))

`goal g_1 :`

forall x,y,z,t:int.

0 <= y + z <= 1 ->

x + t + y + z = 1 ->

y + z <> 0 ->

x + t = 0

`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)

`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)

`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))

`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]

`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

`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

*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.