< Retour au sommaire

Présentation d'Alt-Ergo-Fuzz et Benchpress

Hichem Ait El Hara le

Lieu: Amphi 33, bât 862

Alt-Ergo est un solveur SMT conçu pour la preuve de programmes et utilisé comme backend par différents outils de vérification logicielle comme Frama-C, SPARK, Why3 entre autres. Pour tester de façon efficace cet outil, nous avons développé Alt- Ergo-Fuzz qui est un outil de test par fuzzing conçu pour Alt-Ergo, et dont le but est d’y trouver des bugs. La présentation portera sur la conception d’Alt-Ergo-Fuzz, les résultats des expermentations qui ont été faites avec, les limitations remarquées et les évolutions envisagées. On y présentera aussi benchpress, un outil permettant de lancer des prouveurs automatiques sur des fichiers de test, de visualiser leurs résultats et de les comparer.