Try Alt-Ergo in Your Browser
Recently, we worked on an online Javascript-based serverless version of the Alt-Ergo SMT solver. In what follows, we will explain the principle of this version of Alt-Ergo, show how it can be used on a realistic example and compare its performances with bytecode and native binaries of Alt-Ergo.
Compilation
"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. It is obtained by compiling the bytecode executable of the solver into Javascript thanks to js_of_ocaml. The .js
file is generated following the scheme given below. Roughly speaking, it consists of three steps:
- A new frontend (
main_js.ml
) is added to the sources of Alt-Ergo. This file contains some glue code that allows the generated.js
file to interact with an HTML file (insertion of buttons, modification of DIV contents, ...) - The sources of Alt-Ergo and
main_js.ml
are compiled withocamlc
. The compilation make use of a preprocessor provided byjs_of_ocaml
. - The
js_of_ocaml
compiler is used to transform the bytecode generated byocaml
into a javascript file.
The .js
file is then plugged into an HTML file that fits with the glue code inserted in main_js.ml
.
General overview of the HTML interface
The HTML interface is made of four panels:
- The left panel is an editable textarea in which you can write/past/load the formula you want to prove.
- The bottom-left panel is used to display the answer of Alt-Ergo.
- The middle panel contains a set of buttons that allow to interact with both the interface and the javascript version of Alt-Ergo.
- The right panel is used to display different views. The default view ("Options") allows to control the options of Alt-Ergo. When a formula is proved valid, one may switch to "Statistics" view, thanks to the corresponding button in the middle, to see what are the quantified axioms and predicates that are used/instantiated during the proof. The "Debug" view shows the information received by
main_js.ml
from the HTML interface. The "Examples" view shows some basic examples in Alt-Ergo's native input language that can be loaded in the left panel by a simple click.
A step-by-step example
Let us see how "Try Alt-Ergo" works on a formula translated from Atelier-B in the context of the BWare project:
- First, open Try Alt-Ergo in a new tab/window.
- Download the formula try-alt-ergo.why. This formula contains 177 quantified axioms and 132 predicates.
- Click on the "Load a Local File" button of Try alt-ergo's interface and load the example into the left panel.
- Go to "Options" panel and set the
maximum number of steps
to 1000, themaximum number of triggers
to 1, and deactivateE-matching
- Click on "Ask Alt-Ergo" button and wait approximately 60 seconds (depending on your computer). On my laptop, Alt-Ergo given the following answer after, approximately, 40 seconds.
# Alt-Ergo's answer: Valid (37.2260 seconds) (222 steps)
- Now, you can navigate into the "Statistics" panel to see the quantified axioms and predicates that are instantiated during the proof, those that are potentially used, and those that have never been instantiated.
Limitations
- The Javascript version is slower than native and bytecode versions. In fact, bytecode executable is 4 times faster and native executable is 42 times faster than "Try Alt-Ergo", as shown below.
./alt-ergo.byte -nb-triggers 1 -no-Ematching -max-split infinity -save-used-context try-alt-ergo.why
File "/home/mi/Bureau/po.why", line 3017, characters 1-2450:Valid (9.3105) (222)
./alt-ergo.opt -nb-triggers 1 -no-Ematching -max-split infinity -save-used-context try-alt-ergo.why
File "/home/mi/Bureau/po.why", line 3017, characters 1-2450:Valid (0.8750) (222)
- Since it is not possible to set a time limit in javascript. The "steps" mechanism should be used instead. This limit controls the number of calls to the decision procedure component of the solver.
- Currently, the integration of external plugins (such as our miniSAT-based SAT solver) is not supported
- Compared to AltGr-Ergo, statistics and debug information are only shown at the end of the execution.
- "Asking Alt-Ergo" may report "syntax error" on well formed files for Safari and Midori users. The "Load a Local File" button is not working on Opera browser.
[ Acknowledgement: this work is financially supported by the BWare project. ]
Comments
Joshua Pratt (10 January 2020 at 5 h 20 min):
Can the compiled alt-ergo.js be uploaded to npm? I’d love to use it in a web page I’m working on.
OCamlPro (6 March 2020 at 16 h 03 min):
Hi Joshua, thanks for passing by 🙂 We have no plans of building a bridge between a version of Alt-Ergo in JS and npm. However, you can tweak Alt-Ergo to suit your needs! We would recommend taking a look at Try Why3 http://why3.lri.fr/try/, where you will find a JavaScript version of Alt-Ergo. You can follow their instructions to build Alt-Ergo in JavaScript https://gitlab.inria.fr/why3/why3/tree/master/src/trywhy3
Bharat Jayaraman (26 February 2020 at 17 h 37 min):
This is VERY USEFUL tool!
I am using it in a course on software verification here in Buffalo. It’s great for checking verification conditions.
Many thanks, Bharat
OCamlPro (6 March 2020 at 16 h 04 min):
Hi Bharat! Thank you for your message, we are always glad to hear from our users! If you feel so inclined, you can drop us an email at alt-ergo@ocamlpro.com to tell us more about your experience with Alt-Ergo and any feedback you may have.
About Alt-Ergo
Alt-Ergo is an Open Source automatic solver of mathematical formulas designed for program verification. 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 Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.
This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.
Articles les plus récents
2024
- opam 2.3.0 release!
- Optimisation de Geneweb, 1er logiciel français de Généalogie depuis près de 30 ans
- Alt-Ergo 2.6 is Out!
- Flambda2 Ep. 3: Speculative Inlining
- opam 2.2.0 release!
- Flambda2 Ep. 2: Loopifying Tail-Recursive Functions
- Fixing and Optimizing the GnuCOBOL Preprocessor
- OCaml Backtraces on Uncaught Exceptions
- Opam 102: Pinning Packages
- Flambda2 Ep. 1: Foundational Design Decisions
- Behind the Scenes of the OCaml Optimising Compiler Flambda2: Introduction and Roadmap
- Lean 4: When Sound Programs become a Choice
- Opam 101: The First Steps
2023
- Maturing Learn-OCaml to version 1.0: Gateway to the OCaml World
- The latest release of Alt-Ergo version 2.5.1 is out, with improved SMT-LIB and bitvector support!
- 2022 at OCamlPro
- Autofonce, GNU Autotests Revisited
- Sub-single-instruction Peano to machine integer conversion
- Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
- Release of ocplib-simplex, version 0.5