Release of Alt-Ergo 2.2.0
Authors: 
Date: 2018-04-23
Category: 
Tags: A new release of Alt-Ergo (version 2.2.0) is available.
You can get it from Alt-Ergo's website. An OPAM package for it will be published in the next few days.
The major novelty of this release is a new experimental front-end that supports the SMT-LIB 2 language, extended prenex polymorphism. This extension is implemented as a standalone library, and is available here: https://github.com/Coquera/psmt2-frontend
The full list of CHANGES is available here. As usual, do not hesitate to report bugs, to ask questions, or to give your feedback!
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 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.
Alt-Ergo 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 Alt-Ergo, consider joining the Alt-Ergo user’s Club
Most Recent Articles
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’Alt-Ergo 2021
- New Try-Alt-Ergo
- opam 2.1.0~beta4 released
- opam 2.0.8 release
- 2020 at OCamlPro
- Release of Alt-Ergo 2.4.0
2020