Try Alt-Ergo in Your Browser

Date: 2014-07-15
Category: Formal Methods



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:

try-alt-ergo-compilation

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:

try-alt-ergo-interface

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:

# Alt-Ergo's answer: Valid (37.2260 seconds) (222 steps)

Limitations

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

[ 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 Why playform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI) of the Université Paris Sud and is maintained, developed and distributed since 2013 by the company OCamlPro.

Alt-Ergo is part of the formal method team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP. If you like Alt-Ergo, consider joining the Alt-Ergo user’s Club