Private Release of Alt-Ergo 1.00

Date: 2015-01-29
Category: Formal Methods

altergo logo

After the public release of Alt-Ergo 0.99.1 last December, it's time to announce a new major private version (1.00) of our SMT solver. As usual:

Quick Evaluation

A quick comparison between this new version and the previous releases is given below. Timeout is set to 60 seconds. The benchmark is made of 19044 formulas: (a) some of these formulas are known to be invalid, and (b) some of them are out of scope of current SMT solvers. The results are obtained with Alt-Ergo's native input language.

public release
public release
private release
Proved Valid 15980 16334 17638
Proved Valid (%) 84,01 % 85,77 % 92,62 %
Required time (seconds) 10831 10504 9767
Average speed
(valid formulas per second)
1,47 1,55 1,81

Main Novelties of Alt-Ergo 1.00

General Improvements

Bug Fixes

New OCamlPro Plugins

New Options

Removed Capabilities

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