We are thrilled to share that Alt-Ergo 2.6 has officially been released! Alt-Ergo is an automated prover developped by OCamlPro widely used in formal verification, it plays a key role in static analysis frameworks like the TIS Analyzer, SPARK and Frama-C. This latest version introduces a series of improvements and new features, particularly in bit-vector reasoning, model generation, and optimization. The updates in Alt-Ergo 2.6 are directly tied to the progress made in the DéCySif joint research project between AdaCore, Inria, OCamlPro, and TrustInSoft.

On Tuesday, December 19, 2023, all partners of the Decysif project (TrustInSoft, AdaCore, OCamlPro, and the LMF team) gathered at the TrustInSoft offices in the 14th arrondissement of Paris for the project kickoff meeting! It was a great opportunity to review the ambitious goals of the project, exchange between partners about the organization and agenda of the work. The meeting ended, as is often the case with these well-acquainted partners, with intense technical discussions on the interaction between Why3 (repository) and Alt-Ergo (repository), use cases for testing Creusot (code source), and techniques for detecting vulnerabilities using TIS Analyzer (repository of the OS kernel) or Spark (repository).