./wip/why, Why is a software verification platform

[ CVSweb ] [ Homepage ] [ RSS ] [ Required by ] [ Add to tracker ]

Branch: CURRENT, Version: 2.29, Package name: why-2.29, Maintainer: MarkoSchuetz

Why is a software verification platform.

This platform contains several tools:

1. 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);
2. a tool Krakatoa for the verification of Java programs;
3. 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.).


Required to run:
[lang/ocaml] [devel/nspr] [x11/gtk2] [x11/ocaml-lablgtk] [devel/ocamlgraph]

Required to build:
[pkgtools/x11-links] [x11/xcb-proto] [x11/fixesproto4] [pkgtools/cwrappers] [x11/xorgproto]

Master sites:

RMD160: 2438151fd7ecb309b1a1fb79f09db032b9338c08
Filesize: 2893.532 KB

Version history: (Expand)

CVS history: (Expand)


   2015-07-10 11:50:01 by Thomas Klausner | Files touched by this commit (1) 
Log message:
Update path to ocamlgraph.
   2014-10-10 16:03:21 by Thomas Klausner | Files touched by this commit (3) 
Log message:
Update for lablgtk -> ocaml-lablgtk rename.
   2012-10-07 22:11:06 by Aleksej Saushev | Files touched by this commit (137) 
Log message:
Drop superfluous PKG_DESTDIR_SUPPORT, "user-destdir" is default these days.
Mark packages that don't or might probably not have staged installation.
   2011-05-21 20:27:39 by Marko Schütz Schmuck | Files touched by this commit (4) 
Log message:
initial commit