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

Removing redundant file & replacing relative files

parent 746b217d
......@@ -4,7 +4,7 @@ date=2019-07-09
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 [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/2019_02_11_whats-new-for-alt-ergo-in-2018-here-is-a-recap) 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](2019_02_11_whats-new-for-alt-ergo-in-2018-here-is-a-recap) the SMT-LIB 2 standard.
> Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro and partially funded by R&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)).
>
......@@ -28,23 +28,23 @@ For its first participation in SMT-COMP, Alt-Ergo showed that it was a competiti
</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>
<td><img src="assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_silver.png" alt="2nd place" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
</tr>
</tbody>
</table>
......@@ -58,10 +58,8 @@ Since last year’s competition, we made some improvements on Alt-Ergo, specific
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>
* 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.
* 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>
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.
......@@ -83,31 +81,31 @@ For the last categories, Alt-Ergo managed to reproduce last year’s performance
</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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_gold.png" alt="" width="33" height="33"></td>
<td><img src="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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="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>
......@@ -121,21 +119,21 @@ For the last categories, Alt-Ergo managed to reproduce last year’s performance
<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>
<td><img src="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>
<td><img src="assets/img/icon_gold.png" alt="" width="33" height="33"></td>
<td><img src="assets/img/icon_gold.png" alt="" width="33" height="33"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="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>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
<td><img src="assets/img/icon_bronze.png" alt="" width="24" height="24"></td>
</tr>
</tbody>
</table>
......@@ -145,7 +143,7 @@ This year results are available [here](https://smt-comp.github.io/2019/results.h
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.
![](/assets/img/logo_altergo.png)
![](../assets/img/logo_altergo.png)
### **About Alt-Ergo**
......
......@@ -4,7 +4,7 @@ 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 [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/2019_02_11_whats-new-for-alt-ergo-in-2018-here-is-a-recap) le standard [SMT-LIB 2](http://smtlib.cs.uiowa.edu/).
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](2019_02_11_whats-new-for-alt-ergo-in-2018-here-is-a-recap) le standard [SMT-LIB 2](http://smtlib.cs.uiowa.edu/).
> 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).
>
......@@ -13,4 +13,4 @@ Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop
> _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)_
Voir [ocamlpro.com/blog/alt-ergo-participation-to-the-smt-comp-2019](/blog/2019_07_09_alt-ergo-participation-to-the-smt-comp-2019)
\ No newline at end of file
Voir [ocamlpro.com/blog/alt-ergo-participation-to-the-smt-comp-2019](2019_07_09_alt-ergo-participation-to-the-smt-comp-2019)
\ No newline at end of file
......@@ -4,8 +4,8 @@ date=2020-03-03
category=Formal Methods
tags=alt-ergo
![Alt-Ergo meeting](/blog/assets/img/altergo-meeting.jpeg)
![Logo Alt-Ergo](/assets/img/logo_altergo.png)
![Alt-Ergo meeting](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.
......@@ -13,7 +13,7 @@ La deuxième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu
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 [Why3](http://why3.lri.fr/) avec laquelle nous travaillons pour améliorer nos outils.
Nous remercions tous nos membres pour leur soutien et souhaitons la bienvenue à Mitsubishi Electric R&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 :
......@@ -23,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 [articles](/blog/category/formal_methods) 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](category/formal_methods) sur ce blog.
\ No newline at end of file
title=[Interview] Sylvain Conchon rejoint OCamlPro
authors=Aurore Dromby
date=2020-06-05
category=Formal Methods
tags=alt-ergo
![](/assets/img/photo_sylvain.jpg)
> 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
**Sylvain, tu fréquentes de longue date le monde industriel, que penses-tu des interactions entre les industriels et les laboratoires de recherche ?**
J’ai toujours trouvé très enrichissantes les interactions avec les industriels. Pendant mes études, j’ai travaillé plusieurs années en SSII, et je suis mes étudiants en stage ou en apprentissage dans des sociétés technologiques ou chez de grands industriels. Je participe également à des projets de recherche qui impliquent des industriels,et j’ai passé quelques temps chez Intel à Portland, ce qui m’a permis de découvrir l’industrie du hardware.
**Comment parvenir à établir des relations fructueuses entre le monde académique et les industriels ?**
C’est beaucoup une histoire de rencontre. On le voit lors des montages de projets de recherche collaboratifs qui réunissent académiques et industriels. Les outils issus de la recherche, quels qu’ils soient, doivent avant tout répondre à un besoin réel des industriels. Si c’est le cas, il faut aussi que le logiciel soit utilisable par des ingénieurs du métier sans qu’il leur soit nécessaire de comprendre son fonctionnement interne (par exemple, pour positionner les 50 options nécessaires à son utilisation, interpréter ses résultats ou ses absences de résultats!). Cela nécessite à l’évidence un travail d’ingénierie important, tourné vers l’utilisateur final et souvent éloigné des activités des chercheurs. Il faut donc comprendre les problèmes et les besoins des industriels, et ensuite déterminer si les technologies et les outils que l’on maîtrise peuvent être adaptés ou utilisés pour réaliser un prototype qui réponde à certains de ces besoins.
**Tu viens de rejoindre OCamlPro, quelles sont tes premières impressions ?**
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é !
> _“Les outils issus de la recherche, quels qu’ils soient, doivent avant tout répondre à un besoin réel des industriels.”_
### OCaml, un langage de pointe
**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, _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 ?**
Pendant mes études à l’Université lors de mon projet de fin de maîtrise : un de mes enseignants m’avait orienté vers ce langage pour m’aider à réaliser un compilateur pour un langage de programmation concurrente. J’ai donc découvert ce langage par moi-même, en lisant le manuel et les exemples. Ce n’est que pendant mon DEA que j’ai découvert les fondements théoriques de ce beau langage (sémantique, typage, compilation).
**OCaml, un langage industriel ou pas encore ?**
Il convient de préciser la question : qu’est-ce qu’un langage industriel ? Si c’est un langage utilisé par les industriels, alors OCaml n’est hélas pas encore suffisamment utilisé dans l’industrie pour être qualifié ainsi. Si la question est de savoir s’il a le niveau des langages utilisés dans l’industrie, alors la réponse est oui, sans hésiter. Mais peut-être la question porte-t-elle davantage sur l’écosystème OCaml et la maturité de l’outillage: il y a sûrement des progrès à faire pour atteindre le niveau d’un langage très répandu dans l’industrie, mais c’est en bonne voie, en particulier grâce à des entreprises telles qu’OCamlPro.
### Les méthodes formelles comme technique industrielle, et l’exemple du solveur Alt-Ergo
**Les méthodes formelles sont l’un des domaines d’expertise d’OCamlPro, en quoi penses-tu qu’OCaml est adapté au domaine des SMT ?**
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.
> _“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 ?**
C’est un logiciel utilisé pour prouver automatiquement (sans intervention humaine) des formules logiques, c’est-à-dire savoir si ces formules sont vraies ou fausses. Alt-Ergo appartient à une famille de démonstrateurs automatiques appelée SMT (pour Satisfiabilité Modulo Théories). Il a été conçu pour être intégré dans des plate-formes de vérification de programmes. Ces outils (comme Why3, Frama-C, Spark,…) génèrent des formules logiques qu’il est nécessaire de prouver afin de garantir qu’un programme est sûr. Faire la preuve de ces formules à la main serait très fastidieux (il y a parfois plusieurs dizaines de milliers de formules à prouver). Un solveur SMT comme Alt-Ergo est là pour faire ce travail, de manière complètement automatique. C’est ce qui permet à ces plateformes de vérification d’être utilisables au niveau industriel.
**En quoi le développement d’Alt-Ergo en OCaml peut-il être un avantage par rapport aux concurrents ?**
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.
> _“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 ?**
Les solveurs SMT sont aujourd’hui incontournables dans le domaine de l’ingénierie du logiciel. On les trouve aussi bien dans des outils de preuve, de test, de model checking, d’interprétation abstraite ou encore de typage. La principale raison de ce succès est qu’ils sont de plus en plus efficaces et les théories sous-jacentes sont très expressives. C’est un domaine de recherche très concurrentiel entre les meilleures universités ou laboratoires du monde et de grandes entreprises en informatique. Mais la marge de progression de ces outils est encore très grande, en particulier dans le domaine de l’arithmétique non linéaire où la demande des utilisateurs est de plus en plus forte. Pour le moment, un de mes objectifs en recherche est de combiner les outils de Model Checking avec ceux de preuve de programmes. Ces deux familles d’outils reposent sur les SMT et elles devraient se compléter pour offrir des outils de vérification encore plus automatiques.
**Quelles applications les techniques SMT et Alt-Ergo peuvent-elles avoir dans l’industrie ?**
Les techniques SMT peuvent être utilisées partout où les méthodes formelles peuvent être utiles. Par exemple (mais cette liste est loin d’être exhaustive), pour vérifier la sûreté de logiciels critiques dans le domaine de l’embarqué, pour trouver des failles de sécurité dans les systèmes informatiques ou pour résoudre des problèmes de planification. On les trouve également dans le domaine de l’intelligence artificielle où il est crucial de garantir la stabilité des réseaux de neurones mais aussi de produire des explications formelles sur leurs résultats.
**Tu as été amené à travailler sur le Model Checking, peux-tu nous parler des liens entre Model Checking et SMT et de son utilisation actuelle ?**
Le Model Checking consiste à vérifier que tous les états possibles d’un système respectent bien certaines propriétés, et ce quelles que soient les données en entrée. C’est un problème difficile car certains systèmes (microprocesseurs par ex.) peuvent avoir des centaines de millions d’états. Pour passer à l’échelle, les model checkers implémentent des algorithmes très perfectionnés pour visiter ces états rapidement, en les stockant d’une manière très compacte. Cependant, cette technique atteint ses limites quand les valeurs prises en entrée sont non bornées ou quand le nombre de composants du système n’est pas connu. Pensez aux algorithmes de routage d’Internet où on ne connaît pas le nombre de machines sur le réseau, ces algorithmes doivent être corrects, quel que soit ce nombre de machines. C’est là que les solveurs SMT entrent en jeu. En utilisant des formules logiques, on peut représenter des ensembles d’états de taille arbitraire. Visiter les états d’un système consiste alors à calculer les formules qui représentent ces états. Vérifier que les états respectent une propriété revient à prouver que les formules qui représentent des états impliquent la propriété voulue, etc. Tout dans le Model Checking repose donc sur des formules logiques et les solveurs SMT sont évidemment là pour raisonner sur ces formules.
\ No newline at end of file
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