|
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.
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
|
Why, Krakatoa and Caduceus: Software proof