Commit f2da7428 authored by Steven de Oliveira's avatar Steven de Oliveira
Browse files

Removing HTML (except two big chunks)

parent 96020ac9
......@@ -69,12 +69,14 @@ let rec handle_block = function
| Definition_list (_attr, _attr_def_elt_list) -> ""
let find_preview doc =
String.sub
( String.concat " "
let str = String.concat " "
@@ List.filter
(fun x -> x <> "")
(List.map (fun block -> handle_block block) doc) )
0 300
(List.map (fun block -> handle_block block) doc)
in
try
String.sub str 0 300
with _exn -> str
let preview article_content =
let content = Omd.of_string article_content |> find_preview in
......
......@@ -4,9 +4,11 @@ date=2019-07-9
category=Formal Methods
tags=alt-ergo
The results of the SMT-COMP 2019 were released a few days ago at the SMT whorkshop during the <a href="http://smt2019.galois.com/">22nd SAT conference</a>. We were glad to participate in this competition for the second year in a row, especially as Alt-Ergo <a href="http://ocamlpro.com/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap/">now supports</a> the SMT-LIB 2 standard.
The results of the SMT-COMP 2019 were released a few days ago at the SMT whorkshop during the [22nd SAT conference](http://smt2019.galois.com/). We were glad to participate in this competition for the second year in a row, especially as Alt-Ergo [now supports](/blog/whats-new-for-alt-ergo-in-2018-here-is-a-recap) the SMT-LIB 2 standard.
<blockquote class="wp-block-quote"><p>Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro and partially funded by R&amp;D projects. If you’re interested, please consider joining the <a href="https://alt-ergo.ocamlpro.com/#club">Alt-Ergo User’s Club</a>! Its history goes back in 2006 from early academic researches conducted conjointly at Inria &amp; CNRS “LRI” lab, and the maintenance and development work by OCamlPro since September 2013 (see the <a href="https://alt-ergo.ocamlpro.com/#releases">past releases</a>).</p><p>If you’re curious about OCamlPro’s other activities in Formal Methods, see a happy client’s <a href="http://ocamlpro.com/clients-partners/#mitsubishi-merce">feedback</a>.</p></blockquote>
> Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro and partially funded by R&amp;D projects. If you’re interested, please consider joining the [Alt-Ergo User’s Club](https://alt-ergo.ocamlpro.com/#club)! Its history goes back in 2006 from early academic researches conducted conjointly at Inria & CNRS “LRI” lab, and the maintenance and development work by OCamlPro since September 2013 (see the [past releases](https://alt-ergo.ocamlpro.com/#releases)).
>
> If you’re curious about OCamlPro’s other activities in Formal Methods, see a happy client’s [feedback](/#mitsubishi-merce)
## SMT-COMP 2018
......@@ -16,19 +18,20 @@ Our goal last year was to challenge ourselves on the community benchmarks. We wa
For its first participation in SMT-COMP, Alt-Ergo showed that it was a competitive solver comparing to state of the art solvers such as CVC4, Vampire, VeriT or Z3.
<figure class="wp-block-table"><table><tbody><tr><td>Main Track Categories (number of participants)</td><td>Sequential Perfs</td><td>Parallel Perfs</td></tr><tr><td><a href="http://smtcomp.sourceforge.net/2018/results-ALIA.shtml?v=1531410683">ALIA</a> (4)</td><td><img src="/blog/assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr><tr><td><a href="http://smtcomp.sourceforge.net/2018/results-AUFLIA.shtml?v=1531410683">AUFLIA</a> (4)</td><td><img src="/blog/assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td><td><img src="/blog/assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td></tr><tr><td><a href="http://smtcomp.sourceforge.net/2018/results-AUFLIRA.shtml?v=1531410683">AUFLIRA</a> (4)</td><td><img src="/blog/assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr><tr><td><a href="http://smtcomp.sourceforge.net/2018/results-AUFNIRA.shtml?v=1531410683">AUFNIRA</a> (3)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr></tbody></table></figure>
The global results of the competition are available <a href="http://smtcomp.sourceforge.net/2018/results-toc.shtml">here</a>.
The global results of the competition are available [here](http://smtcomp.sourceforge.net/2018/results-toc.shtml).
## SMT-COMP 2019
Since last year’s competition, we made some improvements on Alt-Ergo, specifically over our data structures and the support of algebraic datatypes (see <a href="http://ocamlpro.com/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap/">post</a>).
Since last year’s competition, we made some improvements on Alt-Ergo, specifically over our data structures and the support of algebraic datatypes (see [post](http://ocamlpro.com/2019/02/11/whats-new-for-alt-ergo-in-2018-here-is-a-recap)).
A few changes can be noted for this year’s competition:
<ol><li>A distinction between SAT and UNSAT in the scoring scheme allowed us to compete in more categories, as Alt-Ergo doesn’t send back SAT.</li><li>The aim of the 24s Scoring is to reward solvers which solve problems quickly.</li><li>The number of benchmarks in each category has changed. For each category, only the benchmarks which were not proven by every solver last year are used. For example: in the division AUFLIRA, 20011 benchmarks were used last year, of which 1683 remained this year.</li></ol>
<ol>
<li>A distinction between SAT and UNSAT in the scoring scheme allowed us to compete in more categories, as Alt-Ergo doesn’t send back SAT.</li><li>The aim of the 24s Scoring is to reward solvers which solve problems quickly.</li>
<li>The number of benchmarks in each category has changed. For each category, only the benchmarks which were not proven by every solver last year are used. For example: in the division AUFLIRA, 20011 benchmarks were used last year, of which 1683 remained this year.</li>
</ol>
Alt-Ergo only competed in the Single Query Track. We selected the same categories as last year and added UF, UFLIA, UFLRA and UFNIA. We also decided to compete over categories supporting algebraic DataTypes to test our newly support of this theory. Alt-Ergo’s expertise is over quantified problems, but we wanted to test our hand in the solver theories over some Quantifier-free categories.
......@@ -40,12 +43,12 @@ For the last categories, Alt-Ergo managed to reproduce last year’s performance
<figure class="wp-block-table"><table><tbody><tr><td>Single Query Categories<br>(number of participants)</td><td>Sequential</td><td>Parallel</td><td>Unsat</td><td>24s</td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/alia-single-query">ALIA</a> (8)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_gold.png" alt="" width="33" height="33"></td><td><img src="/blog/assets/img/icon_silver.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/auflia-single-query">AUFLIA</a> (8)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/auflira-single-query">AUFLIRA</a> (8)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/aufnira-single-query">AUFNIRA</a> (5)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_silver.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/uf-single-query">UF</a> (8)</td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/uflia-single-query">UFLIA</a> (8)</td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="http://ocamlpro.com/wp-content/uploads/2019/07/Copper.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/uflra-single-query">UFLRA</a> (8)</td><td><img src="/blog/assets/img/icon_gold.png" alt="" width="33" height="33"></td><td><img src="/blog/assets/img/icon_gold.png" alt="" width="33" height="33"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_gold.png" alt="" width="33" height="33"></td></tr><tr><td><a href="https://smt-comp.github.io/2019/results/ufnia-single-query">UFNIA</a> (8)</td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td><td><img src="/blog/assets/img/icon_bronze.png" alt="" width="24" height="24"></td></tr></tbody></table></figure>
This year results are available <a href="https://smt-comp.github.io/2019/results.html">here</a>. These results do not include Par4 a portfolio solver.
This year results are available [here](https://smt-comp.github.io/2019/results.html). These results do not include Par4 a portfolio solver.
Alt-Ergo is constantly evolving, as well as our support of the SMT-LIB standard. For next year’s participation, we will try to compete in more categories and hope to cover more tracks, such as the UNSAT-Core track.
<img src="/assets/img/logo_altergo.png" alt="" width="107" height="90">
![](/assets/img/logo_altergo.png)
### <strong>About Alt-Ergo</strong>
### **About Alt-Ergo**
<em>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 <a href="http://why.lri.fr">Why platform</a>. 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 <a href="https://alt-ergo.ocamlpro.com/#club">Alt-Ergo user’s Club</a>.</em>
\ No newline at end of file
_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](http://why.lri.fr). 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](https://alt-ergo.ocamlpro.com/#club)_
\ No newline at end of file
......@@ -4,9 +4,9 @@ date=2020-06-05
category=Formal Methods
tags=alt-ergo
<img src="/assets/img/photo_sylvain.jpg">
![](/assets/img/photo_sylvain.jpg)
<blockquote class="wp-block-quote"><p class="">Sylvain Conchon vient de rejoindre OCamlPro en tant que Chief Scientific Officer Méthodes Formelles. Professeur à l’Université Paris-Saclay, il travaille dans le domaine de la démonstration automatique pour la preuve de programmes et le model checking pour systèmes paramétrés. Il est aussi le co-créateur d’Alt-Ergo.</blockquote>
> Sylvain Conchon vient de rejoindre OCamlPro en tant que Chief Scientific Officer Méthodes Formelles. Professeur à l’Université Paris-Saclay, il travaille dans le domaine de la démonstration automatique pour la preuve de programmes et le model checking pour systèmes paramétrés. Il est aussi le co-créateur d’Alt-Ergo.
### Recherche et industrie
......@@ -22,7 +22,7 @@ C’est beaucoup une histoire de rencontre. On le voit lors des montages de proj
Je suis heureux d’avoir rejoint une entreprise très dynamique, pleine de gens talentueux, motivés et sympathiques, où l’on fait à la fois de l’ingénierie de haut niveau et de la recherche de qualité !
<blockquote class="wp-block-quote"><p class=""><em>Les outils issus de la recherche, quels qu’ils soient, doivent avant tout répondre à un besoin réel des industriels.”</em></blockquote>
> _“Les outils issus de la recherche, quels qu’ils soient, doivent avant tout répondre à un besoin réel des industriels.”_
......@@ -30,7 +30,7 @@ Je suis heureux d’avoir rejoint une entreprise très dynamique, pleine de gens
**Tu es connu dans la communauté OCaml, et certains de tes étudiants sont devenus des fans d’OCaml (et de ton enseignement)… que dis-tu à tes étudiants qui découvrent OCaml ?**
J’ai tendance à résumer en disant ceci : « avec OCaml, vous n’apprenez pas la programmation des 10 dernières années,<em> mais celle des 10 prochaines années ». </em>Cette affirmation s’est toujours vérifiée car bon nombre de traits du langage OCaml se sont retrouvés dans les langages <em>mainstream, </em>avec plusieurs années de décalage. Cela dit, mes années d’expérience dans l’enseignement de ce langage me laissent penser que quelques modifications dans sa syntaxe permettraient une approche plus aisée pour certains débutants.
J’ai tendance à résumer en disant ceci : « avec OCaml, vous n’apprenez pas la programmation des 10 dernières années, _mais celle des 10 prochaines années_ ».Cette affirmation s’est toujours vérifiée car bon nombre de traits du langage OCaml se sont retrouvés dans les langages _mainstream_, avec plusieurs années de décalage. Cela dit, mes années d’expérience dans l’enseignement de ce langage me laissent penser que quelques modifications dans sa syntaxe permettraient une approche plus aisée pour certains débutants.
**Et toi, comment as-tu découvert OCaml ?**
......@@ -46,7 +46,7 @@ Il convient de préciser la question : qu’est-ce qu’un langage industriel ?
Les outils comme les solveurs SMT sont principalement des logiciels de manipulation symbolique des données qui permettent d’analyser, de transformer et de raisonner sur des formules logiques. OCaml est fait pour ce genre de traitements. Il y a aussi une partie plus « calculatoire » dans ces outils qui nécessite une programmation fine des structures de données ainsi qu’une gestion efficace de la mémoire. OCaml est particulièrement adapté pour ce genre de développements, surtout avec son ramasse-miettes (GC) extrêmement performant. Enfin, les solveurs SMT sont des outils qui doivent avoir un grand niveau de fiabilité car les erreurs dans ces logiciels sont difficiles à trouver et leur présence peut être très préjudiciable. Le système de types d’OCaml contribue à la fiabilité de ces outils.
<blockquote class="wp-block-quote"><p class=""><em>“Les solveurs SMT sont aujourd’hui incontournables dans le domaine de l’ingénierie du logiciel.”</em></blockquote>
> _“Les solveurs SMT sont aujourd’hui incontournables dans le domaine de l’ingénierie du logiciel.”_
**Peux-tu nous parler d’Alt-Ergo en quelques mots ?**
......@@ -56,7 +56,7 @@ C’est un logiciel utilisé pour prouver automatiquement (sans intervention hum
Cela lui confère une plus grande sûreté, car un solveur SMT, comme n’importe quel programme peut aussi avoir des bugs. La plus grande partie d’Alt-Ergo est programmée dans un style purement fonctionnel, c’est-à-dire uniquement avec l’utilisation de structures de données immuables. L’un des avantages de ce style de programmation est qu’il nous a permis de prouver formellement ses principaux composants (par exemple, son noyau a été formalisé à l’aide de l’assistant à la preuve Coq, ce qui serait impossible à faire dans un langage comme C++), sans sacrifier son efficacité grâce au très bon ramasse-miettes et à la bibliothèque de structures de données persistantes très performantes d’OCaml. Enfin, nous avons largement bénéficié du système de modules d’OCaml, en particulier les foncteurs et les modules récursifs, pour concevoir un code très modulaire, maintenable et facilement extensible. Au final, OCaml nous a permis de concevoir un solveur SMT aussi performant que CVC4 ou Z3 pour la preuve de programmes, mais avec un nombre de lignes de code divisé par trois ou quatre. Bien sûr, cela ne garantit pas que Alt-Ergo ait zéro bugs, mais cela nous aide beaucoup à mettre le doigt dessus quand quelqu’un en trouve.
<blockquote class="wp-block-quote"><p class=""><em>“OCaml nous a permis de concevoir un solveur SMT aussi performant que CVC4 ou Z3 pour la preuve de programmes, mais avec un nombre de lignes de code divisé par trois ou quatre. “</em></blockquote>
> _“OCaml nous a permis de concevoir un solveur SMT aussi performant que CVC4 ou Z3 pour la preuve de programmes, mais avec un nombre de lignes de code divisé par trois ou quatre. “_
**Quel est ton avis sur les solveurs SMT et l’état de l’art SMT actuel ?**
......
......@@ -4,14 +4,13 @@ date=2019-07-10
category=Formal Methods
tags=alt-ergo
Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop SMT de la <a href="http://smt2019.galois.com/">22e conférence SAT</a>. Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo <a href="/blog/whats-new-for-alt-ergo-in-2018-here-is-a-recap">prend en charge</a> le standard <a href="http://smtlib.cs.uiowa.edu/">SMT-LIB 2</a>.
Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop SMT de la [22e conférence SAT](http://smt2019.galois.com/). Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo [prend en charge](/blog/whats-new-for-alt-ergo-in-2018-here-is-a-recap) le standard [SMT-LIB 2](http://smtlib.cs.uiowa.edu/).
<blockquote>
Alt-Ergo est un SAT solveur open-source maintenu et distribué par OCamlPro, et financé entre autres grâce à plusieurs projets de R&amp;D collaborative (BWare, SOPRANO, Vocal, LChip).
> Alt-Ergo est un SAT solveur open-source maintenu et distribué par OCamlPro, et financé entre autres grâce à plusieurs projets de R&D collaborative (BWare, SOPRANO, Vocal, LChip).
>
> Si vous êtes un utilisateur d’Alt-Ergo, songez à rejoindre le [Club des Utilisateurs d’Alt-Ergo](https://alt-ergo.ocamlpro.com/#club)! L’histoire de ce logiciel remonte à 2006, où il est né de recherches académiques conjointes entre Inria et le CNRS dans le laboratoire du LRI. Il est depuis septembre 2013 maintenu, développé & et distribué par OCamlPro (voir l’historique des [versions passées](https://alt-ergo.ocamlpro.com/#releases)).
>
> _Si vous êtes curieux des activités d’OCamlPro dans le domaine des méthodes formelles, vous pouvez lire le court témoignage d’un [client heureux](http://ocamlpro.com/clients-partners/#mitsubishi-merce)_
Si vous êtes un utilisateur d’Alt-Ergo, songez à rejoindre le <a href="https://alt-ergo.ocamlpro.com/#club">Club des Utilisateurs d’Alt-Ergo</a>! L’histoire de ce logiciel remonte à 2006, où il est né de recherches académiques conjointes entre Inria et le CNRS dans le laboratoire du LRI. Il est depuis septembre 2013 maintenu, développé&nbsp; et distribué par OCamlPro (voir l’historique des <a href="https://alt-ergo.ocamlpro.com/#releases">versions passées</a>).
<em>Si vous êtes curieux des activités d’OCamlPro dans le domaine des méthodes formelles, vous pouvez lire le court témoignage d’un <a href="http://ocamlpro.com/clients-partners/#mitsubishi-merce">client heureux</a>.</em>
</blockquote>
Voir <a href="http://ocamlpro.com/2019/07/09/alt-ergo-participation-to-the-smt-comp-2019/">http://ocamlpro.com/blog/alt-ergo-participation-to-the-smt-comp-2019/</a>
\ No newline at end of file
Voir [ocamlpro.com/blog/alt-ergo-participation-to-the-smt-comp-2019](/blog/alt-ergo-participation-to-the-smt-comp-2019)
\ No newline at end of file
......@@ -4,15 +4,20 @@ date=2021-04-29
category=Formal Methods
tags=alt-ergo
La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.</p>
La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.
<blockquote class="wp-block-quote"><p>Alt-Ergo est un vérificateur automatique de formules mathématiques, développé conjointement par le <a href="https://www.lri.fr/">LRI</a> et OCamlPro (depuis 2014). Pour en savoir plus ou rejoindre le Club, visitez le site <a rel="noreferrer noopener" href="https://alt-ergo.ocamlpro.com/" target="_blank">https://alt-ergo.ocamlpro.com</a>. test</p></blockquote>
> Alt-Ergo est un vérificateur automatique de formules mathématiques, développé conjointement par le [LRI](https://www.lri.fr/) et OCamlPro (depuis 2014). Pour en savoir plus ou rejoindre le Club, visitez le site [https://alt-ergo.ocamlpro.com](https://alt-ergo.ocamlpro.com).
Notre Club a plusieurs objectifs. Son objectif principal est de garantir la pérennité d’Alt-Ergo en favorisant la collaboration entre les membres du Club et en tissant des liens avec les utilisateurs de méthodes formelles, telle que la communauté Why3. L’une de nos priorités est de définir les besoins des utilisateurs de solveurs de contraintes en étendant Alt-Ergo à de nouveaux domaines tels que le Model Checking, tout en concurrençant les autres solveurs de l’état de l’art au cours de compétitions internationales. Enfin, le dernier objectif du Club est de trouver de nouveaux projets ou contrats pour le développement de fonctionnalités à long terme.
Nous tenons à remercier tous nos membres pour leur soutien : Mitsubishi Electric R&amp;D Centre Europe, AdaCore et le CEA List. Nous souhaitons également mettre en lumière l’équipe de développement <a href="http://why3.lri.fr/">Why3</a> avec laquelle nous travaillons pour améliorer nos outils.
Nous tenons à remercier tous nos membres pour leur soutien : Mitsubishi Electric R&amp;D Centre Europe, AdaCore et le CEA List. Nous souhaitons également mettre en lumière l’équipe de développement [Why3](http://why3.lri.fr/) avec laquelle nous travaillons pour améliorer nos outils.
Cette année, de nouveaux points d’intérêts ont été soulevés par nos membres. Dans un premier temps, la génération de modèles, ajoutée à Alt-Ergo suite à la dernière édition, a été utile à la majorité des membres du club. Les points techniques souhaités à présent sont de pouvoir raffiner les contraintes et étudier comment les propager. Dans un second temps a eu lieu la présentation de Dolmen, le parseur/typer qui permettra de ne typer qu’une seule fois les fichiers SMT2 et d’être prêt pour le SMT3. Son intégration à Alt-Ergo est en cours, l’avis des membres du club est enthousiaste sur les apports futurs de l’outil Dolmen à la communauté des solveurs SMT ! <br><br>Ces fonctionnalités sont désormais nos principales priorités, retrouvez <a href="https://gitlab.ocamlpro.com/OCamlPro/club-alt-ergo_ext/-/blob/master/Planche_Club_Alt-Ergo_Edition2021.pdf?inline=false">les planches</a> présentées à la réunion du Club édition 2021. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos <a href="https://www.ocamlpro.com/category/alt-ergo/">articles</a> sur notre blog.
Cette année, de nouveaux points d’intérêts ont été soulevés par nos membres. Dans un premier temps, la génération de modèles, ajoutée à Alt-Ergo suite à la dernière édition, a été utile à la majorité des membres du club. Les points techniques souhaités à présent sont de pouvoir raffiner les contraintes et étudier comment les propager. Dans un second temps a eu lieu la présentation de Dolmen, le parseur/typer qui permettra de ne typer qu’une seule fois les fichiers SMT2 et d’être prêt pour le SMT3. Son intégration à Alt-Ergo est en cours, l’avis des membres du club est enthousiaste sur les apports futurs de l’outil Dolmen à la communauté des solveurs SMT !
<blockquote class="wp-block-quote"><p><strong>About OCamlPro:</strong></p><p>OCamlPro is a R&amp;D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, <a href="http://try.ocamlpro.com">TryOCaml</a>, ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our <a href="https://alt-ergo.ocamlpro.com/#club">Alt-Ergo Users’ Club</a>). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: <a href="mailto:contact@ocamlpro.com">contact@ocamlpro.com</a>.</p></blockquote>
\ No newline at end of file
Ces fonctionnalités sont désormais nos principales priorités, retrouvez [les planches](https://gitlab.ocamlpro.com/OCamlPro/club-alt-ergo_ext/-/blob/master/Planche_Club_Alt-Ergo_Edition2021.pdf?inline=false) présentées à la réunion du Club édition 2021. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](https://www.ocamlpro.com/category/alt-ergo/) sur notre blog.
> **About OCamlPro:**
>
> OCamlPro is a R&D lab founded in 2011, with the mission to help industrial users benefit from state-of-the art programming languages like OCaml and Rust. We design, create and implement custom ad-hoc software for our clients. We also have a long experience in developing and maintaining open-source tooling for OCaml, such as Opam, [TryOCaml](http://try.ocamlpro.com), ocp-indent, ocp-index and ocp-browser, and we contribute to the core-development of OCaml, notably with our work on the Flambda optimizer branch. Another area of expertise is that of Formal Methods, with tools such as our SMT Solver Alt-Ergo (check our [Alt-Ergo Users'](https://alt-ergo.ocamlpro.com/#club)). We also provide vocational trainings in OCaml and Rust, and we can build courses on formal methods on-demand. Do not hesitate to reach out by email: [contact@ocamlpro.com](mailto:contact@ocamlpro.com).
......@@ -4,17 +4,16 @@ date=2020-03-03
category=Formal Methods
tags=alt-ergo
<img src="/blog/assets/img/altergo-meeting.jpeg">
<img src="/assets/img/logo_altergo.png">
![Alt-Ergo meeting](/blog/assets/img/altergo-meeting.jpeg)
![Logo Alt-Ergo](/assets/img/logo_altergo.png)
La deuxième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu à la mi-février ! Notre réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Cette année, nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de route concernant les développements et les améliorations futures d’Alt-Ergo.
<blockquote class="wp-block-quote"><p>Alt-Ergo est un vérificateur automatique de formules mathématiques, développé conjointement par le <a href="https://www.lri.fr/">LRI</a> et OCamlPro (depuis 2014). Pour en savoir plus ou rejoindre le Club, visitez le site <a rel="noreferrer noopener" href="https://alt-ergo.ocamlpro.com/" target="_blank">https://alt-ergo.ocamlpro.com</a>.</p></blockquote>
> Alt-Ergo est un vérificateur automatique de formules mathématiques, développé conjointement par le [LRI](https://www.lri.fr/) et OCamlPro (depuis 2014). Pour en savoir plus ou rejoindre le Club, visitez le site [https://alt-ergo.ocamlpro.com/](https://alt-ergo.ocamlpro.com).
Notre Club a plusieurs objectifs, le premier étant de garantir la pérennité d’Alt-Ergo en favorisant la collaboration entre les membres du Club et en renforçant la collaboration avec les communautés de méthodes formelles telles que Why3. L’une de nos priorités est d’augmenter le nombre d’utilisateurs de notre outil en l’étendant à de nouveaux domaines tels que le Model Checking, la participation à des compétitions internationales étant également un moyen de gagner en visibilité. Enfin, le dernier objectif du Club est de trouver de nouveaux projets ou contrats pour le développement de fonctionnalités à long terme.
Nous remercions tous nos membres pour leur soutien et souhaitons la bienvenue à Mitsubishi Electric R&amp;D Centre Europe qui rejoint AdaCore et le CEA List en tant que membre du Club cette année. Nous souhaitons également mettre en lumière l’équipe de développement <a href="http://why3.lri.fr/">Why3</a> avec laquelle nous travaillons pour améliorer nos outils.
Nous remercions tous nos membres pour leur soutien et souhaitons la bienvenue à Mitsubishi Electric R&amp;D Centre Europe qui rejoint AdaCore et le CEA List en tant que membre du Club cette année. Nous souhaitons également mettre en lumière l’équipe de développement [Why3](http://why3.lri.fr/) avec laquelle nous travaillons pour améliorer nos outils.
Nos membres sont particulièrement intéressés par les points suivants :
......@@ -24,4 +23,4 @@ Nos membres sont particulièrement intéressés par les points suivants :
– L’amélioration du support de l’arithmétique non linéaire dans Alt-Ergo
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos <a href="/blog/category/formal_methods">articles</a> sur ce blog.
\ No newline at end of file
Ces fonctionnalités sont maintenant nos principales priorités. Pour suivre nos avancement et les nouveautés, n’hésitez pas à lire nos [articles](/blog/category/formal_methods) sur ce blog.
\ No newline at end of file
......@@ -10,7 +10,7 @@ After the hard work done on the integration of floating-point arithmetic reasoni
As you may know, Alt-Ergo’s native input language is not compliant with the SMT-LIB 2 input language standard, and translating formulas from SMT-LIB 2 to Alt-Ergo’ syntax (or vice-versa) is not immediate. Besides its extension with polymorphism, this native language diverges from SMT-LIB’s by distinguishing terms of type <code>boolean</code> from formulas (that are <code>propositions</code>). This distinction makes it hard, for instance, to efficiently translate <code>let-in</code> and <code>if-then-else</code> constructs that are ubiquitous in SMT-LIB 2 benchmarks.
In order to work closely with the SMT community, we designed a conservative extension of the SMT-LIB 2 standard with <code>prenex polymorphism</code> and implemented it as a new frontend in Alt-Ergo 2.2. This work has been published in the 2018 edition of the SMT-Workshop. An online version of the paper is <a href="https://hal.inria.fr/hal-01960203" target="_blank" rel="noopener noreferrer">available here</a>. Experimental results showed that polymorphism is really important for Alt-Ergo, as it allows to improve both resolution rate and resolution time (see Figure 5 in the paper for more details).
In order to work closely with the SMT community, we designed a conservative extension of the SMT-LIB 2 standard with <code>prenex polymorphism</code> and implemented it as a new frontend in Alt-Ergo 2.2. This work has been published in the 2018 edition of the SMT-Workshop. An online version of the paper is [available here](https://hal.inria.fr/hal-01960203). Experimental results showed that polymorphism is really important for Alt-Ergo, as it allows to improve both resolution rate and resolution time (see Figure 5 in the paper for more details).
## Improved SAT solvers
......@@ -22,11 +22,11 @@ As emphasized above, we published our work regarding polymorphic SMT2 and SAT so
Thanks to our new SMT2 frontend, we were able to participate to the SMT-Competition last year. Naturally, we selected categories that are close to “deductive program verification”, as Alt-Ergo is primarily tuned for formulas coming from this application domain.
Although Alt-Ergo <a href="http://smtcomp.sourceforge.net/2018/results-summary.shtml?v=1531410683" target="_blank" rel="noopener noreferrer">did not rank first</a>, it was a positive experience and this encourages us to go ahead. Note that Alt-Ergo’s brother, Ctrl-Ergo, was not far from winning <a href="http://smtcomp.sourceforge.net/2018/results-QF_LIA.shtml" target="_blank" rel="noopener noreferrer">the QF-LIA category</a> of the competition. This performance is partly due to the improvements in the CDCL SAT solver that were also integrated in Ctrl-Ergo.
Although Alt-Ergo [did not rank first](http://smtcomp.sourceforge.net/2018/results-summary.shtml?v=1531410683), it was a positive experience and this encourages us to go ahead. Note that Alt-Ergo’s brother, Ctrl-Ergo, was not far from winning [the QF-LIA category](http://smtcomp.sourceforge.net/2018/results-QF_LIA.shtml) of the competition. This performance is partly due to the improvements in the CDCL SAT solver that were also integrated in Ctrl-Ergo.
## Alt-Ergo for Atelier-B
<a href="https://www.atelierb.eu/en/" target="_blank" rel="noopener noreferrer">Atelier-B</a> is a framework that allows to develop formally verified software using <a href="https://www.methode-b.com/en/b-method/" target="_blank" rel="noopener noreferrer">the B Method</a>. The framework rests on an automatic reasoner that allows to discharges thousands of mathematical formulas extracted from B models. If a formula is not discharged automatically, it is proved interactively. <a href="https://www.clearsy.com/en/" target="_blank" rel="noopener noreferrer">ClearSy</a> (the company behind development of Atelier-B) has recently added a new backend to produce verification conditions in Why3’s logic, in order to target more automatic provers and increase automation rate. For certifiability reasons, we extended Alt-Ergo with a new frontend that is able to directly parse these verification conditions without relying on Why3.
[Atelier-B](https://www.atelierb.eu/en/) is a framework that allows to develop formally verified software using [the B Method](https://www.methode-b.com/en/b-method/). The framework rests on an automatic reasoner that allows to discharges thousands of mathematical formulas extracted from B models. If a formula is not discharged automatically, it is proved interactively. [ClearSy](https://www.clearsy.com/en/) (the company behind development of Atelier-B) has recently added a new backend to produce verification conditions in Why3’s logic, in order to target more automatic provers and increase automation rate. For certifiability reasons, we extended Alt-Ergo with a new frontend that is able to directly parse these verification conditions without relying on Why3.
## Improved hash-consed data-structures
......@@ -60,6 +60,6 @@ goal g:
In 2018, we welcomed a lot of new engineers with a background in formal methods: Steven (De Oliveira) holds a PhD in formal verification from the Paris-Saclay University and the French Atomic Energy Commission (CEA). He has a master in cryptography and worked in the Frama-C team, developing open-source tools for verifying C programs. David (Declerck) obtained a PhD from Université Paris-Saclay in 2018, during which he extended the Cubicle model checker to support weak memory models and wrote a compiler from a subset of the x86 assembly language to Cubicle. Guillaume (Bury) holds a PhD from Université Sorbonne Paris Cité. He studied the integration of rewriting techniques inside SMT solvers. Albin (Coquereau) is working as a PhD student between OCamlPro, LRI and ENSTA, focusing on improving the Alt-Ergo SMT solver. Adrien is interested in verification of safety properties over software and embedded systems. He worked on higher-order functional program verification at the University of Tokyo, and on the Kind 2 model checker at the University of Iowa. All these people will consolidate the department of formal methods at OCamlPro, which will be beneficial for Alt-Ergo.
In 2019 we just launched the Alt-Ergo Users’ Club, in order to get closer to our users, collect their needs, and integrate them into the Alt-Ergo roadmap, but also to ensure sustainable funding for the development of the project. We are happy to announce the very first member of the Club is <a href="https://www.adacore.com" target="_blank" rel="noopener noreferrer">Adacore</a>, very soon to be followed by <a href="https://trust-in-soft.com" target="_blank" rel="noopener noreferrer">Trust-In-Soft</a> and <a href="http://www-list.cea.fr/en/" target="_blank" rel="noopener noreferrer">CEA List</a>. Thanks for your early support!
In 2019 we just launched the Alt-Ergo Users’ Club, in order to get closer to our users, collect their needs, and integrate them into the Alt-Ergo roadmap, but also to ensure sustainable funding for the development of the project. We are happy to announce the very first member of the Club is [Adacore](https://www.adacore.com), very soon to be followed by [Trust-In-Soft](https://trust-in-soft.com) and [CEA List](http://www-list.cea.fr/en/). Thanks for your early support!
> Interested to join? Contact us: contact@ocamlpro.com
\ No newline at end of file
......@@ -101,7 +101,7 @@ We cater to very specific needs. For example, we can translate a “black box”
<p>
Starting from a specification provided by MERCE, we designed and implemented a formal verification analysis tool to check a particular class of safety properties over C programs. The tool was implemented as a Frama-C plug-in and came with fully fledged user and formal documentation.
</p>
<figure class="quote">
<figure class="quote" id="mitsubishi-merce">
<blockquote class="text-end">
<p>
“MERCE was very satisfied of OCamlPro. The project was technically challenging and time constrained, nonetheless OCamlPro met the requirements in time while producing a code of excellent quality.”
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment