Alt-Ergo: the SMT solver with model generation
The Alt-Ergo automatic theorem prover developed at OCamlPro has just been released with a major update : counterexample model can now be generated. This is now available on the next branch, and will officially be part of the 2.5.0 release, coming this year !
Alt-Ergo at a Glance
Alt-Ergo is an open source automatic theorem prover based on the SMT technology. It was born at the Laboratoire de Recherche en Informatique, Inria Saclay Ile-de-France and CNRS in 2006 and has been maintained and developed by OCamlPro since 2013.
It is capable of reasoning in a combination of several built-in theories such as:
- uninterpreted equality;
- integer and rational arithmetic;
- arrays;
- records;
- algebraic data types;
- bit vectors.
It also is able to deal with commutative and associative operators, quantified formulas and has a polymorphic first-order native input language. Alt-Ergo is written in OCaml. Its core has been formally proved in the Coq proof assistant.
Alt-Ergo has been involved in a qualification process (DO-178C) by Airbus Industrie. During this process, a qualification kit has been produced. It was composed of a technical document with tool requirements (TR) that gives a precise description of each part of the prover, a companion document (~ 450 pages) of tests, and an instrumented version of the tool with a TR trace mechanism.
Model Generation
When a property is false, generating a counterexample is a key that many state-of-the-art SMT-solvers should include by default. However, this is a complex problem in the first place.
The first obstacle is the decidability of the theories manipulated by the SMT solvers. In general, the complexity class (i.e. the classification of algorithmic problems) is between "NP-Hard" (for the linear arithmetic theory on integers for example) and "Undecidable" (for the polynomial arithmetic on integers for example). Then comes the quantified properties, i.e. properties prefixed with forall
s and exists
, adding an additional layer of complexity and undecidability. Another challenge was the core algorithm behind Alt-Ergo which does not natively support model generation. At last, an implementation of the models have to take care of Alt-Ergo's support of polymorphism.
How to use Model Generation in Alt-Ergo
There are two ways to activate model generation on Alt-Ergo.
- Basic usage: simply add the option
--model
to your command ($ alt-ergo file --model
) - Advanced usage: three options mainly impact the model generation.
-
--interpretation
: sets the model generation strategy. It can either benone
for no model generation;first
for generating the very first interpretation computed only;every
for generating a model after each decision andlast
only generating a model whenalt-ergo
concludes on the formula satisfiability. -
--sat-solver
: only the 'Tableaux-CDCL' sat solver is compatible with the interpretation feature -
--instantiation-heuristic
: when set tonormal
,alt-ergo
generates model faster. This is an experimental feature that sometimes generates incorrect models.Example:
$ alt-ergo file --interpretation every --sat-solver Tableaux-CDCL --instantiation-heuristic auto
-
Warning: only the linear arithmetic and the enum model generation have been
tested. Other theories are either not implemented (ADTs) or experimental (risk
of crash or unsound models). We are currently still heavily testing the
feature, so feel free to join us on
Alt-Ergo's GitHub repository if you have
questions or issues with this new feature.
Note that the models generated are best-effort models; Alt-Ergo
does not answer Sat
when it outputs a model. In a future version, we will add
a mechanism that automatically checks the model generated.
Godspeed!
Acknowledgements
We want to thank David Mentré and Denis Cousineau at Mitsubishi Electric R&D Center Europe for funding the initial work on counterexample.
Note that MERCE has been a Member of the Alt-Ergo Users’ Club for 3 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. Please do not hesitate to contact the Alt-Ergo team at OCamlPro: alt-ergo@ocamlpro.com.
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
- 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