Centre de recherche Inria de Saclay

Why3

Un langage pour la vérification déductive de programmes

Why3 est une boîte à outils pour la preuve mathématique de programmes, applicable à la vérification de systèmes critiques. Elle permet de prouver formellement qu’un code a le comportement attendu.

La vérification d’un programme par preuve formelle consiste à transformer simultanément le code source et son comportement attendu en un ensemble d’énoncés mathématiques : les obligations de preuve. Il s’agit ensuite d’établir la véracité de ces énoncés à l’aide de logiciels de démonstration automatiques ou semi-automatiques. Cette méthode réduit le temps des tests et donc les coûts de la vérification.

L’originalité de Why3 réside dans son adaptabilité, lui permettant d’être intégré dans différents logiciels pour la vérification de systèmes embarqués : il peut disposer de plusieurs langages d’entrées (C, Java, Ada, OCaml) et est capable d’exploiter de nombreux prouveurs en sortie (automatiques et/ou interactifs).

Une collaboration réussie

Why3 a, par exemple, été intégrée au cœur de l’environnement SPARK*, développé par la société AdaCore**, pour la vérification de codes critiques écrits en langage Ada. Cette intégration s’est déroulée dans le cadre du LabCom ProofInUse entre l’équipe Toccata et AdaCore.

Aujourd’hui, les projets clients SPARK ont des applications aussi variées que :

• les systèmes de gestion de trafic aérien
• la mise en œuvre à haute fiabilité de composants de véhicule
• le développement de logiciel embarqué fiable pour la santé (cœur artificiel de la société Scandinavian Real Heart AB)

La technologie Why3 est également utilisée dans l’environnement Frama-C pour l’analyse de codes critiques écrits en langage C, développé au CEA-LIST.

* SPARK : Technologie de vérification formelle
** Adacore : PME éditrice de logiciels spécialisée dans la fourniture d’outils de développement pour les systèmes critiques

 

Fiche technique

  • Equipe-Projet : Toccata
  • Licence : LGPL
  • Langage : OCaml
Domaines d'applications :
Industrie

Industrie
Défense & sécurité

Défense & sécurité
Outils multidomaines

Outils multidomaines

Démonstration du logiciel Why3

Testez le logiciel

Introduction à l’activité de preuve formelle et à l’utilisation de Why3 :

Paroles de partenaires

Lorsque nous avons cherché en 2010 à moderniser notre outil d’analyse formelle de programmes, nous nous sommes naturellement tournés vers l’équipe Toccata qui développait déjà l’outil Why et qui avait montré son avance scientifique et sa maturité technologique lors d’expériences d’adoption industrielle réussies. Le choix fait par l’équipe Toccata de développer des logiciels sous licence libre et leur soutien continu aux utilisateurs industriels ont été déterminants dans le succès de cette aventure commune.

Cyrille Comar,
Président d’AdaCore 

Ils nous font confiance

Devenez partenaire du centre Inria de Saclay

Contactez-nous pour échanger sur votre besoin

L'équipe Toccata

Toccata

Toccata est une équipe de recherche du centre Inria
Saclay-Île-de-France, en partenariat avec le Laboratoire Méthodes Formelles (Université Paris-Saclay, CNRS, ENS Paris-Saclay, Inria et CentraleSupélec)

L’objectif général de l’équipe est de promouvoir la spécification formelle et la preuve assistée par ordinateur dans le développement de logiciels qui exigent des garanties élevées de sa sécurité et de sa
conformité vis-à-vis de son comportement prévu.
L’équipe travaille sur la conception de méthodes et d’outils de vérification déductive des programmes. Une de ses compétences originales est la capacité de mener des preuves en utilisant simultanément des prouveurs automatiques et des assistants de preuve, en fonction de la difficulté du programme, et plus particulièrement de la difficulté de chaque condition de
vérification.