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 foralls 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 be none for no model generation; first for generating the very first interpretation computed only; every for generating a model after each decision and last only generating a model when alt-ergo concludes on the formula satisfiability.

  • --sat-solver: only the 'Tableaux-CDCL' sat solver is compatible with the interpretation feature

  • --instantiation-heuristic: when set to normal, 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.