Lambda the Ultimate

inactiveTopic Why, Krakatoa and Caduceus: Software proof
started 4/15/2004; 4:08:03 PM - last post 4/15/2004; 4:08:03 PM
Jim Apple - Why, Krakatoa and Caduceus: Software proof  blueArrow
4/15/2004; 4:08:03 PM (reads: 112, responses: 0)
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


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