Why: asoftware verification platform

Time 2021-10-16 23:03:48

Web Name: Why: asoftware verification platform

WebSite: http://why.lri.fr

ID:205447

Keywords:

asoftware,Why,platform,verification,programverificationformalproofobligations

Description:

keywords:program verification formal proof obligations
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.

WhyWhy is a software verification platform.

This platform contains several tools:a general-purpose verification condition generator (VCG),Why, whichis 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.).DocumentationUser manual, inPostScript andHTML.

Introduction to the Why tool given at theTYPES Summer School2007 :slides;lecture notes;exercises.

Examples of programs certified with Why are collectedon this page.

Why is presented in this article.Theoretical foundations are described in this paper.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:

Opam packages Distributed source code archives: see here Anonymous access to the development version

Requirements: 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.4

There is anEclipse pluginfor Why/Caduceus/Krakatoa.

To download/install theorem provers, look at the Prover Tips pageSMT-lib benchmarksA set of SMT-lib benchmarks from our test suites:Why Benchmarks.Related toolsKrakatoa, a tool on top of Why and Coq to certify JML-annotated Java programs, by Claude Marché, Christine Paulin, Nicolas Rousset and Xavier UrbainCaduceus, a tool on top of Why to certify C programs, byJean-ChristopheFilliâtre, Thierry Hubert and Claude Marché ; now obsolete and subsumed by Frama-CFrama-C, a general environment for static analysis of C programs, which uses Why has a plugin (plugin Jessie, by Yannick Moy and Claude Marché)For back-end provers, please look at the Prover Tips pageContactThere 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".Credits The main developers of the Why platform areJean-ChristopheFilliâtre, Claude Marché, Yannick Moy, Thierry Hubert, Nicolas Rousset Also have contributed to development:Romain Bardou, Jean-François Couchot, Mehdi Dogguy, Christine Paulin, Yann Régis-Gianas, Xavier UrbainYasuhiko 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:asoftware Why platform verification programverificationformalproofobligations

<<< Thank you for your visit >>>

Hot Websites