Project Summary
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.).
Quick Reference
- Project Links:
-
Homepage
Download
- Code Locations:
-
https://www.lri.fr/svn/demons/wh...
- Licenses:
- LGPL-2.1+
- Similar Projects:
-
- Managers:
- Claude Marché and Jean-Christophe Filliatre
In a Nutshell, Why...
- ...
- ...
-
...
has a well established, mature codebase
maintained by a average size development team
with increasing Y-O-Y commits -
...
took an estimated 87 years of effort (COCOMO model)
starting with its first commit in August, 2001
ending with its most recent commit 21 days ago
Activity
30 Day Summary May 15 2013 — Jun 14 2013
|
12 Month Summary Jun 14 2012 — Jun 14 2013
|
Community
Copyright
©
2013
Black Duck Software, Inc.
and its contributors, Some Rights Reserved. Unless otherwise marked, this work is licensed under a
Creative Commons Attribution 3.0 Unported License
. Ohloh
®
and the Ohloh logo are trademarks of
Black Duck Software, Inc.
in the United States and/or other jurisdictions. All other trademarks are the property of their respective holders.