-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
add ae 2.6 article, add pop art alt ergo visual
- Loading branch information
1 parent
35d3973
commit 8475250
Showing
5 changed files
with
185 additions
and
0 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,40 @@ | ||
--- | ||
date: 2024-10-18T11:22:33Z | ||
description: "**Alt-Ergo 2.6 is sponsored by DéCySif**" | ||
featured_image: '/images/Decysif.png' | ||
thumbnail: '/images/alt-ergo-8-colors-blank-bg.png' | ||
tags: ["Alt-Ergo", "Prover", "Bit-Vector", "Model Generation", "Optimization", "Release"] | ||
title: "Alt-Ergo 2.6 Release: Boosting Formal Verification with New Features" | ||
--- | ||
|
||
We are thrilled to share that **Alt-Ergo 2.6** has officially been released! | ||
|
||
Alt-Ergo is an automated prover developped by [OCamlPro](https://ocamlpro.com/) | ||
widely used in formal verification and plays a key role in static analysis | ||
frameworks like the [TIS | ||
Analyzer](https://www.trust-in-soft.com/trustinsoft-analyzer) and | ||
[Frama-C](https://frama-c.com/). | ||
|
||
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](https://www.adacore.com/), | ||
[Inria](https://www.inria.fr/en/toccata), OCamlPro, and | ||
[TrustInSoft](https://www.trust-in-soft.com/). | ||
|
||
### What's New? | ||
|
||
- Enhanced support for **bit-vectors** and **algebraic data types**. | ||
- New **optimization capabilities** to guide solver behavior. | ||
- **Model generation** for a broader range of theories, including bit-vectors. | ||
|
||
These updates are particularly valuable for those working on low-level code | ||
verification, cryptography, or complex system debugging. | ||
|
||
For a deeper dive into the release, including performance comparisons and | ||
additional features, visit the full release notes over on [OCamlPro's | ||
Blog](https://ocamlpro.com/blog/2024_09_01_alt_ergo_2_6_0_released/). | ||
|
||
Don't miss out on this powerful upgrade to Alt-Ergo! | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,47 @@ | ||
--- | ||
date: 2024-10-18T11:22:33Z | ||
description: "**Alt-Ergo 2.6 est sponsorisé par DéCySif**" | ||
featured_image: '/images/Decysif.png' | ||
thumbnail: '/images/alt-ergo-8-colors-blank-bg.png' | ||
tags: ["Alt-Ergo", "Prover", "Bit-Vector", "Génération de Modèles", "Optimisation", "Release"] | ||
title: "Sortie d'Alt-Ergo 2.6 : Renforcer la vérification formelle avec de nouvelles fonctionnalités" | ||
--- | ||
|
||
Nous sommes ravis d'annoncer la sortie officielle d'**Alt-Ergo 2.6** ! | ||
|
||
Alt-Ergo est un prouveur SMT automatique développé par | ||
[OCamlPro](https://ocamlpro.com/), largement utilisé en vérification formelle, | ||
jouant un rôle clé dans les cadres d'analyse statique tels que le [TIS | ||
Analyzer](https://www.trust-in-soft.com/trustinsoft-analyzer) et | ||
[Frama-C](https://frama-c.com/). | ||
|
||
Cette nouvelle version introduit une série d'améliorations et de nouvelles | ||
fonctionnalités, en particulier dans le raisonnement sur les bit-vectors, la | ||
génération de modèles et l'optimisation. | ||
|
||
Les mises à jour d'Alt-Ergo 2.6 sont directement liées aux avancées réalisées | ||
dans le cadre du projet de recherche conjoint **DéCySif** entre | ||
[AdaCore](https://www.adacore.com/), | ||
[Inria](https://www.inria.fr/en/toccata), [OCamlPro](https://ocamlpro.com/) et | ||
[TrustInSoft](https://www.trust-in-soft.com/). | ||
|
||
### Quoi de neuf ? | ||
|
||
- Un support amélioré pour les **bit-vectors** et les **types de données | ||
algébriques**. | ||
- De nouvelles **capacités d'optimisation** pour guider le comportement du | ||
démonstrateur. | ||
- La **génération de modèles** pour un éventail plus large de théories, y | ||
compris les bit-vectors. | ||
|
||
Ces améliorations sont particulièrement utiles pour ceux qui travaillent sur la | ||
vérification de code bas-niveau, la cryptographie ou le débogage de systèmes | ||
complexes. | ||
|
||
Pour en savoir plus sur cette version, y compris les comparaisons de | ||
performances et les autres fonctionnalités, consultez les notes de version | ||
complètes sur le [Blog | ||
d'OCamlPro](https://ocamlpro.com/blog/2024_09_01_alt_ergo_2_6_0_released/). | ||
|
||
Ne manquez pas cette mise à jour puissante d'Alt-Ergo ! | ||
|
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
[more] | ||
other = "More" | ||
|
||
[allTitle] | ||
other = "All {{.Title }}" | ||
|
||
[recentTitle] | ||
other = "Recent {{.Title }}" | ||
|
||
[readMore] | ||
other = "read more" | ||
|
||
[by] | ||
other = "By" | ||
|
||
[whatsInThis] | ||
other = "What's in this {{ .Type }}" | ||
|
||
[related] | ||
other = "Related" | ||
|
||
[yourName] | ||
other = "Your Name" | ||
|
||
[emailAddress] | ||
other = "Email Address" | ||
|
||
[message] | ||
other = "Message" | ||
|
||
[emailRequiredNote] | ||
other = "An email address is required." | ||
|
||
[send] | ||
other = "Send" | ||
|
||
[taxonomyPageList] | ||
other = "Below you will find pages that utilize the taxonomy term “{{ .Title }}”" | ||
|
||
[readingTime] | ||
one = "One minute read" | ||
other = "{{ .Count }} minutes read" | ||
|
||
[wordCount] | ||
one = "One word" | ||
other = "{{ .Count }} words" | ||
|
||
[pageTitle] | ||
other = "{{ .Name }} page" |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,49 @@ | ||
[more] | ||
other = "Plus" | ||
|
||
[allTitle] | ||
other = "Tous les {{.Title }}" | ||
|
||
[recentTitle] | ||
other = "{{.Title }} récentes" | ||
|
||
[readMore] | ||
other = "lire plus" | ||
|
||
[by] | ||
other = "Par" | ||
|
||
[whatsInThis] | ||
other = "Ce qui est dans {{ .Type }}" | ||
|
||
[related] | ||
other = "Lié" | ||
|
||
[yourName] | ||
other = "Votre nom" | ||
|
||
[emailAddress] | ||
other = "Adresse e-mail" | ||
|
||
[message] | ||
other = "Message" | ||
|
||
[emailRequiredNote] | ||
other = "Une adresse e-mail est requise." | ||
|
||
[send] | ||
other = "Envoyer" | ||
|
||
[taxonomyPageList] | ||
other = "Ci-dessous se trouvent les pages utilisant le terme taxonomique “{{ .Title }}”" | ||
|
||
[readingTime] | ||
one = "Une minute de lecture" | ||
other = "{{ .Count }} minutes de lecture" | ||
|
||
[wordCount] | ||
one = "Un mot" | ||
other = "{{ .Count }} mots" | ||
|
||
[pageTitle] | ||
other = "{{ .Name }} page" |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.