Private Release of AltErgo 1.00
After the public release of AltErgo 0.99.1 last December, it's time to announce a new major private version (1.00) of our SMT solver. As usual:
 we freely provide a JavaScript version on AltErgo's website
 we provide a private access to our internal repositories for academia users and our clients.
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 AltErgo's native input language.
public release 0.95.2 
public release 0.99.1 
private release 1.00 


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 AltErgo 1.00
General Improvements
 theories data structures: semantic values (internal theories representation of terms) are now hashconsed. This enables the use of hashbased comparison (instead of structural comparison) when possible
 theories combination: the dispatcher component, that sends literals assumed by the SAT solver to different theories depending on whether these literals are equalities, disequalities or inequalities, has been reimplemented. The new code is much more simpler and enables some optimizations and factorizations that could not be made before
 casesplit analysis: we made several improvements in the heuristics of the casesplit analysis mechanism over finite domains
 explanations propagation: we improved explanations propagation in congruence closure and linear arithmetic algorithms. This makes the proofs faster thanks to a better backjumping in the SAT solver part
 linear integer arithmetic: we reimplemented several parts of linear arithmetic and introduced important improvements in the FourierMotzkin algorithm to make it run on smaller subproblems and avoid some useless executions. These optimizations allowed a significant speed up on our internal benchmarks
 data structures: we optimized hashconsing and some functions in the "formula" and "literal" modules
 SAT solving: we made a lot of improvements in the default SATsolver and in the SatML plugin. In particular, the solvers now send lists of facts (literals) to "the decision procedure part" instead of sending them one by one. This avoids intermediate calls to some "expensive" algorithms, such as FourierMotzkin
 Matching: we extended the Ematching algorithm to also perform matching modulo the theory of records. In addition, we simplified matching heuristics and optimized the Ematching process to avoid computing the same instances several times
 Memory management: thanks to the ocpmemprof tool (http://memprof.typerex.org/), we identified some parts of AltErgo that needed some improvements in order to avoid useless memory allocations, and thus unburden the OCaml garbage collector
 the function that retrieves the used axioms and predicates (when option 'saveusedcontext' is activated) has been improved
Bug Fixes
 6 in the "inequalities" module of linear arithmetic
 4 in the "formula" module
 3 in the "ty" module used for types representation and manipulation
 2 in the "theories frontend" module that interacts with the SAT solvers
 1 in the "congruence closure" algorithm
 1 in "existential quantifiers elimination" module
 1 in the "typechecker"
 1 in the "AC theory" of associative and commutative function symbols
 1 in the "unionfind" module
New OCamlPro Plugins
 profiling plugin: when activated, this plugin records and prints some information about the current execution of AltErgo every 'x' seconds: In particular, one can observe a module being activated, a function being called, the amount of time spent in every module/function, the current decision/instantiation level, the number of decisions/instantiations that have been made so far, the number of casesplits, of boolean/theory conflicts, of assumptions in the decision procedure, of generated instances per axiom, ….
 fmsimplex plugin: when activated, this plugin is used instead of the FourierMotzkin method to infer bounds for linear integer arithmetic affine forms (which are used in the casesplit analysis process). This module uses the Simplex algorithm to simulate particular runs of FourierMotzkin, which makes it scale better on linear integer arithmetic problems containing a lot of inequalities
New Options

versioninfo: prints some information about this version of AltErgo (release and compilation dates, release commit ID)

notheory: deactivate theory reasoning. In this case, only the SATsolver and the matching parts are working

inequalitiesplugin: specify a plugin to use, instead of the "default" FourierMotzkin algorithm, to handle inequalities of linear arithmetic

tightenvars: when this option is set, the FmSimplex plugin will try to infer bounds for integer variables as well. Note that this option may be very expensive

profilingplugin: specify a profiling plugin to use to monitor an execution of AltErgo

profiling
: makes the profiling module prints its information every seconds 
notcp: deactivate constraints propagation modulo theories
Removed Capabilities
 the pruning module used in the frontend is now removed
 the SMT and SMT2 frontends are removed. We plan to implement a new frontend for SMT2 in upcoming releases
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 platform. 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 methods team here at OCamlPro. This work is partially funded by the research projects Soprano, BWare, Vocal and LCHIP and the AltErgo Users' Club members. If you like AltErgo, consider joining the AltErgo user’s Club.
Articles les plus récents
2024
 Flambda2 Ep. 3: Speculative Inlining
 opam 2.2.0 release!
 Flambda2 Ep. 2: Loopifying TailRecursive 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 LearnOCaml to version 1.0: Gateway to the OCaml World
 The latest release of AltErgo version 2.5.1 is out, with improved SMTLIB and bitvector support!
 2022 at OCamlPro
 Autofonce, GNU Autotests Revisited
 Subsingleinstruction Peano to machine integer conversion
 Statically guaranteeing security properties on Java bytecode: Paper presentation at VMCAI 23
 Release of ocplibsimplex, version 0.5
 The Growth of the OCaml Distribution