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,
HOL Light, Mizar and the decision procedures haRVey and|
Currently, Why is used by the tools Krakatoa (verification of
Java programs) and Caduceus (verification of C programs).
I removed a font tag, since the post wasn't readable. -- Ehud