Why

If you are looking for an all-in-one software for code verification, Why might be what you need. The software packs a variety of tools including a general-purpose verification condition generator (VCG) that serves as a backend for other verification tools, as well as a tool Krakatoa for verifying Java programs, and Caduceus for C programs (though it is somewhat obsolete now).

One of the standout features of Why is its interoperability with several existing provers and decision procedures like Coq, HOL 4, HOL Light, PVS, Isabelle/HOL, Mizar, Simplify, Alt-Ergo, Z3, CVC3, and Yices. With this level of integration, users can enjoy a seamless verification experience when using any of the supported provers.

Direct use of Why for program verification is also an option. The software offers a wide range of examples to guide users, and support is available for both Java and C programs. Finally, Krakatoa and Caduceus can function as standalone tools but are also available as part of Why, giving users access to even more verification options.