Software verification tool for C and Java
DescriptionWhy 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, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
Upload more screenshots
Please help extend the collection of screenshots. Just make a screenshot and upload it here. You don't need to register or anything.Upload a screenshot
Hint: upload an image here from your clipboard with Ctrl-V
Install this software package
If the package is available for the distribution you are currently using on your computer then install the software by clicking on…Install why