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.
Most Recent Articles
2024
- Archéologie de la Généalogie: prise en main et optimisation d’un logiciel vieux 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
- The Growth of the OCaml Distribution