Why
Why is a software verification tool.
Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligations for many systems: the proof assistants Coq, PVS, HOL Light, Mizar and the decision procedures haRVey and Simplify.
[ Homepage ]
| Author: | Jean-Christophe Filliātre. |
| Last modification date: | 29-Sep-2003 |
| Version: | 1.42 |
| Development status: | Stable |
| Kind: | Applications written in Caml :: Scientific software |
| License: | Open Source :: GPL |
| Topic: | Programming languages :: Program analysis |
| Homepage: | http://why.lri.fr/index.en.html |