Debian logoDebian Screenshots >

why

Software verification tool

Software verification tool
from version 2.26+dfsg-2+b2

Description

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, 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.


Homepage

http://why.lri.fr/


Statistics

71 other people were interested in this package here. The newest known version of this software is 2.34-4+b1 (Information last updated about 11 hours ago.)