Package: why (2.30+dfsg-5 and others)
Links for why
Download Source Package why:
- Homepage [why.lri.fr]
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, Isabelle/HOL, HOL 4, HOL Light, Mizar and the decision procedures Simplify, Alt-Ergo, Yices, CVC Lite and haRVey.
Other Packages Related to why
- dep: frama-c-base (= 20111001+nitrogen+dfsg-4)
- Framework for C source code analysis (without gui)
- dep: make
- An utility for Directing compilation.
- rec: alt-ergo
- Automatic theorem prover dedicated to program verification
- sug: libwhy-coq (= 2.30+dfsg-5+b1)
- Why library for Coq