Alt-Ergo 2.6 is Out!

---

We are excited to announce the release of Alt-Ergo 2.6!

Alt-Ergo is an open-source automated prover used for formal verification in software development. It is part of the arsenal behind static analysis frameworks such as TrustInSoft Analyzer and Frama-C, and is one of the solvers behind Why3, a platform for deductive program verification. The newly released version 2.6 brings new features and performance improvements.

Development on Alt-Ergo has accelerated significantly this past year, thanks to the launch of the DéCySif joint research project (i-Démo) with AdaCore, Inria, OCamlPro and TrustInSoft. The improvements to bit-vectors and algebraic data types in this release are sponsored by the Décysif project.

The highlights of Alt-Ergo 2.6 are:

• Support for reasoning and model generation with bit-vectors
• Model generation for algebraic data types
• Optimization with (maximize) and (minimize)
• FPA support is enabled by default and available in SMT-LIB format
• Binary releases now on GitHub

Alt-Ergo 2.6 also includes other improvements to the user interface (notably the set-option SMT-LIB command), use of Dolmen as the default frontend for SMT-LIB and native input, and many bug fixes.

Bit-vectors

In Alt-Ergo 2.5, we introduced built-in functions for the bit-vector primitives from the SMT-LIB standard, but only provided limited reasoning support. For Alt-Ergo 2.6, we set out to improve this reasoning support, and have developed a new and improved relational theory for bit-vectors. This new theory is based on an also new constraint propagation core that draws heavily on the architecture of the Colibri solver (as in Sharpening Constraint Programming approaches for Bit-Vector Theory), integrated into Alt-Ergo's existing normalizing Shostak solver.

Bit-vectors are commonly used in verification of low-level code and in cryptography, so improved support significantly enhances Alt-Ergo’s applicability in these domains.

There are still areas of improvements, so please share any issue you encounter with the bit-vector theory (or Alt-Ergo in general) via our issue tracker.

To showcase improvements in Alt-Ergo 2.6, we compared it against the version 2.5 and industry-leading solvers Z3 and CVC5 on a dataset of bit-vector problems collected from our partners in the DéCySif project. The (no BV) variants for Alt-Ergo do not use the new bit-vector theory but instead an axiomatization of bit-vector primitives provided by Why3. The percentages represent the proportion of bit-vector problems solved successfully in each configuration.

	AE 2.5		AE 2.6		Z3 (4.12.5)	CVC5 (1.1.2)	Total
	(BV)	(no BV)	(BV)	(no BV)
#	4128	4870	6265	4940	5482	7415	9038
%	46%	54%	69%	54%	61%	82%	100%

As the table shows, Alt-Ergo 2.6 significantly outperforms version 2.5, and the new built-in bit-vector theory outperforms Why3's axiomatization. We even surpass Z3 on this benchmark, a testament to the new bit-vector theory in Alt-Ergo 2.6.

Model Generation

Bit-vector is not the only theory Alt-Ergo 2.6 improves upon. Model generation was introduced in Alt-Ergo 2.5 with support for booleans, integers, reals, arrays, enumerated types, and records. Alt-Ergo 2.6 extends this support to bit-vector and arbitrary algebraic data types, which means that model generation is now enabled for all the theories supported by Alt-Ergo.

Model generation allows users to extract concrete examples or counterexamples, aiding in debugging and verification of their systems.

Model generation is also more robust in Alt-Ergo 2.6, with numerous bug fixes and improvements for edge cases.

Optimization

Alt-Ergo 2.6 introduces optimization capabilities, available via SMT-LIB input using OptiSMT primitives such as (minimize) and (maximize) and compatible with Z3 and OptiMathSat. Optimization allows guiding the solver towards simpler and smaller counterexamples, helping users find more concrete and realistic scenarios to trigger a bug.

See some examples in the documentation.

SMT-LIB command support

Alt-Ergo 2.6 supports more SMT-LIB syntax and commands, such as:

• The (get-info :all-statistics) command to obtain information about the solver's statistics
• The (reset), (exit) and (echo) commands
• The (get-assignment) command, as well as the :named attribute and :produce-assignments option

See the SMT-LIB standard for more details about these commands.

Floating-point theory

In this release, we have made Alt-Ergo's floating-point theory enabled by default: there is no need to provide the --enable-theories fpa flag anymore. The theory can be disabled with --disable-theories fpa,nra,ria (the nra and ria theories were automatically enabled along with the fpa theory in Alt-Ergo 2.5).

We have also made the floating-point primitives available in the SMT-LIB format as the indexed constant ae.round and the convenience ae.float16, ae.float32, ae.float64 and ae.float128 functions; see the documentation.

Dolmen is the new default frontend

Introduced in Alt-Ergo 2.5, the Dolmen frontend has been rigorously tested for regressions and is now the default for both .smt2 and .ae files; the --frontend dolmen flag that was introduced in Alt-Ergo 2.5 is no longer necessary.

The Dolmen frontend is based on the Dolmen library developed by Guillaume Bury at OCamlPro. It provides excellent support for the SMT-LIB standard and is used to check validity of all new problems in the SMT-LIB benchmark collection, as well as the results of the annual SMT-LIB affiliated solver competition SMT-COMP.

The preferred input format for Alt-Ergo is now the SMT-LIB format. The legacy .ae format is still supported, but is now deprecated and users are encouraged to migrate to the SMT-LIB format if possible. Please reach out if you find any issue while migrating to the SMT-LIB format.

As we announced when releasing Alt-Ergo 2.5, the legacy frontend (supports .ae files only) is deprecated in Alt-Ergo 2.6, but it can still be enabled with the --frontend legacy option. It will be removed entirely from Alt-Ergo 2.7.

Parser extensions, such as the built-in AB-Why3 plugin, only work with the legacy frontend, and will no longer work with Alt-Ergo 2.7. We are not aware of any current users of either parser extensions or the AB-Why3 plugin: if you need these features, please reach out to us on GitHub or by email so that we can figure out a path forward.

Use of dune-site for plugins

Starting with Alt-Ergo 2.6, we are using the plugin mechanism from dune-site to replace the custom plugin loading Dynlink. Plugins now need to be registered in the (alt-ergo plugins) site with the plugin stanza.

This does not impact users, but only impacts developers of Alt-Ergo plugins. See the dune file for Alt-Ergo's built-in FM-Simplex plugin for reference.

Binary releases on GitHub

Starting with Alt-Ergo 2.6, we will be providing binary releases on the GitHub Releases page for Linux (x86_64) and macOS (x86_64 and arm). These are released under the same licensing conditions as the Alt-Ergo source code.

The binary releases are statically linked and have no dependencies, except for system dependencies on macOS. They do not support dynamically loading plugins.

Performance

For Alt-Ergo 2.6, our main focus of improvement in term of reasoning was on bit-vectors and algebraic data types. Other theories also benefit from broader performance improvements we made. On our internal problem dataset, Alt-Ergo 2.6 is about 5% faster than Alt-Ergo 2.5 on the goals they both prove.

And more!

This release also includes significant internal refactoring, notably a rewrite from scratch of the interval domain. This improves the accuracy of Alt-Ergo in handling interval arithmetic and facilitates mixed operations involving integers and bit-vectors, resulting in shorter and more reliable proofs.

See the complete changelog here.

We encourage you to try out Alt-Ergo 2.6 and share your experience or any feedback on our GitHub or by email at alt-ergo@ocamlpro.com. Your input will help share future releases!

Acknowledgements

We thank the Alt-Ergo Users' Club members: AdaCore, the CEA, Thales, Mitsubishi Electric R&D Center Europe (MERCE) and TrustInSoft.

Special thanks to David Mentré and Denis Cousineau at MERCE for funding the initial optimization work. MERCE has been a Member of the Alt-Ergo Users' Club for four years. This partnership allowed Alt-Ergo to evolve and we hope that more users will join the Club on our journey to make Alt-Ergo a must-have tool.

---

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.