New Try-Alt-Ergo

---

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation.

This playground website has been maintained by OCamlPro for many years, and it's high time to bring it back to life with new updates. We are therefore pleased to announce the new version of the Try-Alt-Ergo website! In this article, we will first explain what has changed in the back end, and what you can use if you are interested in running your own version of Alt-Ergo on a website, or in an application! And then we will focus on the new front-end of our website, from its interface to its features through its tutorial about the program.* *

Try-Alt-Ergo 2014

Try-Alt-Ergo was designed to be a powerful and simple tool to use. Its interface was minimalist. It offered three panels, one panel (left) with a text area containing the problem to prove. The centered panel was composed of a button to run Alt-Ergo, load examples, set options. The right panel showed these options, examples and other information. This design lacked some features that have been added to our solver through the years. Features such as models (counter-examples), unsat-core, more options and debug information was missing in this version.

Try-Alt-Ergo did not offer a proper editor (with syntax coloration), a way to save the file problem nor an option to limit the run of the solver with a time limit. Another issue was about the thread. When the solver was called the webpage froze, that behavior was problematic in case of the long run because there was no way to stop the solver.

Alt-Ergo 1.30

The 1.30 version of Alt-Ergo was the version used in the back-end to prove problems. Since this version, a lot of improvements have been done in Alt-Ergo. To learn more about these improvements, see our changelog in the documentation.

Over the years we encountered some difficulties to update the Alt-Ergo version used in Try-Alt-Ergo. We used Js_of_ocaml to compile the OCaml code of our solver to be runnable as a JavaScript code. Some libraries were not available in JavaScript and we needed to manually disable them. The lack of automatism leads to a lack of time to update the JavaScript version of Alt-Ergo in Try-Alt-Ergo.

In 2019 we switched our build system to dune which opens the possibility to ease the cross-compilation of Alt-Ergo in JavaScript.

New back-end

With some simple modification, we were able to compile Alt-Ergo in JavaScript. This modification is simple enough that this process is now automated in our continuous integration. This will enable us to easily provide a JavaScript version of our Solver for each future version.

Two ways of using our solver in JavaScript are available:

• alt-ergo.js, a JavaScript version of the Alt-Ergo CLI. It can be runned with node: node alt-ergo.js <options> <file>. Note that this code is slower than the natively compiled CLI of Alt-Ergo.In our effort to open the SMT world to more people, an npm package is the next steps of this work.
• alt-ergo-worker.js, a web worker of Alt-Ergo. This web worker needs JSON file to input file problem, options into Alt-Ergo and to returns its answers:
  • Options are sent as a list of couple name:value like:{"debug":true,"input_format":"Native","steps_bound":100,"sat_solver": "Tableaux","file":"test-file"}You can specify all options used in Alt-Ergo. If some options are missing, the worker uses the default value for these options. For example, if debug is not specified the worker will use its defaults value :false.- Input file is sent as a list of string, with the following format:{ "content": [ "goal g: true"] }
  • Alt-Ergo answers can be composed with its results, debug information, errors, warnings …{ "results": [ "File "test-file", line 1, characters 9-13: Valid (0.2070) (0 steps) (goal g) ] ,``"debugs": [ "[Debug][Sat_solver]", "use Tableaux-like solver"] }like the options, a result value like debugs does not contains anything, "debugs": [...] is not returned.
  • See the Alt-Ergo web-worker documentation to learn more on how to use it.

New Front-end

The Try-Alt-Ergo has been completely reworked and we added some features:

• The left panel is still composed in an editor and answers area
  • Ace editor with custom syntax coloration (both native and smt-lib2) is now used to make it more pleasant to write your problems.
• A top panel that contains the following buttons:
  • Ask Alt-Ergo which retrieves content from the editor and options, launch the web worker and print answers in the defined areas.
  • Load and Save files.
  • Documentation, that sends users to the newly added native syntax documentation of Alt-Ergo.
  • Tutorial, that opens an interactive tutorial to introduce you to Alt-Ergo native syntax and program verification.

• A right panel composed of tabs:
  • Start and About that contains general information about Alt-Ergo, Try-Alt-Ergo and how to use it.
  • Outputs prints more information than the basic answer area under the editor. In these tabs you can find debugs (long) outputs, unsat-core or models (counter-example) generated by Alt-Ergo.
  • Options contains every option you can use, such as the time limit / steps limit or to set the format of the input file to prove .
  • Statistics is still a basic tab that only output axioms used to prove the input problem.
  • Examples contains some basic examples showing the capabilities of our solver.

We hope you will enjoy this new version of Try-Alt-Ergo, we can't wait to read your feedback!

This work was done at OCamlpro.

---

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.