Why
Why is a software verification platform.
This platform contains several tools:
- a general-purpose verification condition generator (VCG),
Why, which
is used as a back-end by other verification tools (see below) but
which can also be used directly to verify programs
(see for instance these examples) ;
- a tool Krakatoa for the verification of Java programs;
- a tool Caduceus for the verification of C programs; note that
Caduceus is somewhat obsolete now and users should turn to
Frama-C instead.
One of the main features of Why is to be integrated with many
existing provers (proof assistants such as Coq,
PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar and
decision procedures such as Simplify, Alt-Ergo, Yices, Z3,
CVC3, etc.).
Documentation
User manual, in
PostScript and
HTML.
Introduction to the Why tool given at the
TYPES Summer School
2007 :
slides
;
lecture notes
;
exercises.
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 LIBRARY GENERAL PUBLIC LICENSE (with a
special exception for linking; see the LICENSE file included in the
source distribution).
It is available as:
Here are the recent changes.
You download previous versions from the FTP zone.
Requirements:
- to compile the sources, you need Objective Caml 3.09 (or higher)
- to compile the graphical user interface gwhy (optional but highly
recommanded) you also need the
Lablgtk2 library (Note that there is a Debian package, liblablgtk2-ocaml-dev).
- no prover is distributed with Why, you must install at least one supported prover from the list below
- if you are willing to use Coq as a back-end prover, you
need at least Coq version 7.4
There is an
Eclipse plugin
for Why/Caduceus/Krakatoa.
To download/install theorem provers, look at the Prover Tips page
SMT-lib benchmarks
A set of SMT-lib benchmarks from our test suites:
Why Benchmarks.
Related tools
- Krakatoa,
a tool on top of Why and Coq to certify
JML-annotated Java programs, by Claude Marché, Christine Paulin, Nicolas Rousset and Xavier Urbain
- Caduceus,
a tool on top of Why to certify
C programs, by
Jean-Christophe
Filliâtre, Thierry Hubert and Claude Marché ;
now obsolete and subsumed by Frama-C
- Frama-C,
a general environment for static analysis of C programs, which uses Why has a plugin (plugin Jessie, by Yannick Moy and Claude Marché)
For back-end provers, please look at the Prover Tips page
Contact
There is a
mailing
list for Why (to ask questions about Why, to get
announces of new releases, etc.).
For bug reports, please use the
bug tracking system. For
security reasons, you need to register before submitting a new
bug. Please create an account there, where you can put "ProVal" for
the required field "INRIA Research Project you work with or work in".
Credits
-
The main developers of the Why platform are
Jean-Christophe
Filliâtre,
Claude Marché,
Yannick Moy,
Thierry Hubert,
Nicolas Rousset
-
Also have contributed to development:
Romain Bardou, Jean-François Couchot, Mehdi Dogguy, Christine Paulin, Yann Régis-Gianas, Xavier Urbain
- Yasuhiko Minamide developped the output for Isabelle/HOL
- Seungkeol Choe developped the output for HOL 4
-
Useful feedback was provided by
M. Levy, N. Magaud, C. Paulin, S. Ranise, L. Théry,
X. Urbain, F. Wiedijk, S. Boldo, G. Melquiond, ... (sorry for the ones we forget to mention)
-
Michel
Levy and César Muñoz contributed to Why's PVS library
