La plateforme Why n'est plus développée. Notre effort s'est porté vers le développement de Why3.

Why est toujours maintenu, en particulier pour fournir le plug-in Jessie de Frama-C et l'outil Krakatoa pour Java. Merci de consulter la page spécifique à Krakatoa et Jessie pour plus de détails.

Nous invitons les autres utilisateurs de Why à migrer vers Why3. Un petit guide de migration est fourni. Se rapporter à la documentation de Why3 pour plus de détails.





Why

Why est une plateforme de vérification de programmes.

Cette plateforme contient plusieurs outils :

L'un des points forts de la plateforme Why est son intégration de nombreux pouveurs existants, comme les asistants de preuve Coq, PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar, et les démonstrateurs automatiques Simplify, Alt-Ergo, Yices, Z3, CVC3, etc.

Documentation

Manuel utilisateur, au format PostScript et HTML (en anglais).

Introduction à l'outil Why donnée à l'école d'été TYPES Summer School 2007 : transparents ; notes de cours ; exercices.

Des exemples de programmes certifiés avec Why sont rassemblés sur cette page.

L'outil Why est présenté dans cet article. Le support théorique de cet outil est décrit dans cette thèse.

Distribution

Why est distribué librement, sous la licence GNU LIBRARY GENERAL PUBLIC LICENSE (avec une exception ; cf le fichier LICENSE inclus dans la distribution). Il est disponible sous forme de :

Voici les derniers changements.

Vous pouvez récupérer des versions antérieures en accédant directement à la zone FTP.

Accès anonyme à la version de développement :

  svn --username guest co https://www.lri.fr/svn/demons/why2/trunk/

Pré-requis:

Il existe un Plugin Eclipse pour Why/Caduceus/Krakatoa.

To download/install theorem provers, look at the Prover Tips page

SMT-lib benchmarks

Un ensemble de benchmarks SMT-lib tirés de nos outils : Why Benchmarks.

Outils connexes

For back-end provers, please look at the Prover Tips page

Contact

Il y a une liste de diffusion pour Why où sont faites notamment les annonces de nouvelles distributions. Les bugs doivent être signalés en utilisant lesystème de rapport de bugs. Pour soumettre un bug, il faut d'abord créer un compte, en mentionnant "ProVal" dans le champ "INRIA Research Project you work with or work in".

Crédits


American