Why3, une plateforme pour la vérification déductive (original) (raw)

Communication Dans Un Congrès Année : 2023

Résumé

Dans cet exposé, nous présentons l'outil Why3, une plateforme pour la vérification déductive de programmes développée au Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS Paris-Saclay / Inria Saclay). Cette plateforme est utilisée dans les milieux académiques et industriels pour la vérification d'algorithmes, de codes écrits dans langages tels que C, Ada ou OCaml, ou encore la vérification de protocoles cryptographiques. La plateforme Why3 est également exploitée pour enseigner la vérification de programmes. Cet exposé met en avant les atouts de la plateforme Why3 et décrit le coeur de métier de son équipe de développement.

Connectez-vous pour contacter le contributeur

https://inria.hal.science/hal-04060570

Soumis le : jeudi 6 avril 2023-11:50:32

Dernière modification le : vendredi 24 octobre 2025-16:40:02

Archivage à long terme le : vendredi 7 juillet 2023-18:34:40

Dates et versions

hal-04060570 , version 1 (06-04-2023)

Licence

Identifiants

Citer

Jean-Christophe Filliâtre. Why3, une plateforme pour la vérification déductive. Journées FAC 2023, groupe IFSE du RTRA STAE, Apr 2023, Toulouse, France. ⟨hal-04060570⟩

679 Consultations

282 Téléchargements