Why: a software verification platform

Time 2020-12-28 18:03:07

Web Name: Why: a software verification platform

WebSite: http://why.lri.fr

ID:149120

Keywords:

software,Why,platform,

Description:

The Why platform is not any longer under active development. Our efforthas moved to the development of Why3.Why is still maintained, in particular to provide the Jessie plug-inof Frama-C and the Krakatoa front-end for Java. Please refer to the specific web page for Krakatoa and Jessie for more details.We invite Why users to move toWhy3. A quick migration guide isprovided. Refer to the Why3 documentation for further details.is used as a back-end by other verification tools (see below) butwhich can also be used directly to verify programs(see for instance these examples) ;a tool Krakatoa for the verification of Java programs;a tool Caduceus for the verification of C programs; note thatCaduceus is somewhat obsolete now and users should turn toFrama-C instead.One of the main features of Why is to be integrated with manyexisting provers (proof assistants such as Coq,PVS, Isabelle/HOL, HOL 4, HOL Light, Mizar anddecision procedures such as Simplify, Alt-Ergo, Yices, Z3,CVC3, etc.).DownloadWhy is freely available, under the terms of the GNU LIBRARY GENERAL PUBLIC LICENSE (with aspecial exception for linking; see the LICENSE file included in thesource distribution).It is available as: to compile the sources, you need OCaml 3.09 (or higher) to compile the graphical user interface gwhy (optional but highlyrecommended) you also need the Lablgtk2 library (Note that there is a Debian package, liblablgtk2-ocaml-dev). no prover is distributed with Why, you must install at least one supported prover from the list below if you are willing to use Coq as a back-end prover, youneed at least Coq version 7.4To download/install theorem provers, look at the Prover Tips pageSMT-lib benchmarksThere is amailinglist for Why (to ask questions about Why, to getannounces of new releases, etc.).For bug reports, please use thebug tracking system. Forsecurity reasons, you need to register before submitting a newbug. Please create an account there, where you can put "Toccata" forthe required field "INRIA Research Project you work with or work in".Yasuhiko Minamide developped the output for Isabelle/HOLSeungkeol Choe developped the output for HOL 4 Useful feedback was provided by M. Levy, N. Magaud, C. Paulin, S. Ranise, L. Théry, X. Urbain, F. Wiedijk, S. Boldo, G. Melquiond, ... (sorry for the ones we forget to mention) Michel Levy and César Muñoz contributed to Why's PVS library

TAGS:software Why platform 

<<< Thank you for your visit >>>

Hot Websites