 | WhyA free software verification platform |
| Download | |
Why Ranking & Summary
Advertisement
- License:
- GPL
- Price:
- FREE
- Publisher Name:
- Why Team
- Publisher web site:
- http://why.lri.fr/
- Operating Systems:
- Mac OS X
- File Size:
- 2.6 MB
Why Tags
Why Description
A free software verification platform Why 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, HOL 4, HOL Light, PVS, Isabelle/HOL, Mizar and decision procedures such as Simplify, Alt-Ergo, Z3, CVC3, Yices, etc.). Requirements: · Objective Caml 3.09 or later What's New in This Release: · Fixed 'Not_found' exception if .whyrc absent · Fixed installation problems. · predicates for finiteness of floats (is_finite, · is_infinite, etc.) do not fail in mode JessieFloatModel(real) but · give the expected truth value. · do not fail anymore on pointer casts over floats or reals. · Fixes bug 273 of Frama-C BTS
Why Related Software