Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, HOL Light, Mizar and the decision procedures haRVey and Simplify.
Currently, Why is used by the tools Krakatoa (verification of Java programs) and Caduceus (verification of C programs).
Note that the Why language can be used directly to verify programs; see for instance these examples.
Examples of programs certified with Why are collected on this page.
Why is presented in this article.
Theoretical foundations are described in this paper.
Download
Why is freely available, under the terms of the GNU GENERAL PUBLIC LICENSE.
It is available as:
Previous versions:
You can access the FTP zone directly. Here are the recent changes.