AltErgo: the SMT solver with model generation
The AltErgo 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 !
AltErgo at a Glance
AltErgo is an open source automatic theorem prover based on the SMT technology. It was born at the Laboratoire de Recherche en Informatique, Inria Saclay IledeFrance and CNRS in 2006 and has been maintained and developed by OCamlPro since 2013.
It is capable of reasoning in a combination of several builtin 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 firstorder native input language. AltErgo is written in OCaml. Its core has been formally proved in the Coq proof assistant.
AltErgo has been involved in a qualification process (DO178C) 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 stateoftheart SMTsolvers 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 "NPHard" (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 AltErgo which does not natively support model generation. At last, an implementation of the models have to take care of AltErgo's support of polymorphism.
How to use Model Generation in AltErgo
There are two ways to activate model generation on AltErgo.
 Basic usage: simply add the option
model
to your command ($ altergo 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 whenaltergo
concludes on the formula satisfiability. 
satsolver
: only the 'TableauxCDCL' sat solver is compatible with the interpretation feature 
instantiationheuristic
: when set tonormal
,altergo
generates model faster. This is an experimental feature that sometimes generates incorrect models.Example:
$ altergo file interpretation every satsolver TableauxCDCL instantiationheuristic 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
AltErgo's GitHub repository if you have
questions or issues with this new feature.
Note that the models generated are besteffort models; AltErgo
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 AltErgo Users’ Club for 3 years. This partnership allowed AltErgo to evolve and we hope that more users will join the Club on our journey to make AltErgo a musthave tool. Please do not hesitate to contact the AltErgo team at OCamlPro: altergo@ocamlpro.com.
About AltErgo
AltErgo is an opensource automatic solver of mathematical formulas designed for program verification. AltErgo 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.
AltErgo 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 AltErgo, consider joining the AltErgo user’s Club
Articles les plus récents
2023
2022
2021
 Verification for Dummies: SMT and Induction
 Generating static and portable executables with OCaml
 opam 2.1.0 is released!
 opam 2.0.9 release
 Detecting identity functions in Flambda
 Détection de fonctions d’identité dans Flambda
 opam 2.1.0~rc2 released
 Tutorial: Format Module of OCaml
 Réunion annuelle du Club des utilisateurs d’AltErgo 2021
 New TryAltErgo