Managed Projects

Why

  No analysis available

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 ... [More] 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.). [Less]

0 lines of code

0 current contributors

0 since last commit

2 users on Open Hub

Activity Not Available
5.0
 
I Use This
Mostly written in language not available
Licenses: lgpl21_or...