Commit 33503e93 authored by MARCHE Claude's avatar MARCHE Claude
Browse files


parent 2323809a
Why3 is a tool for automated and interactive proving in first-order
polymorphic logic. It provides a collection of command-line tools, a
graphical interface and an Objective Caml library.
The documentation (a tutorial and a reference manual) is in
the file doc/manual.pdf.
Various examples can be found in the subdirectories theories/ and
Mailing list (Why3 Club):
Bug Tracking System:
This program is distributed under the GNU LGPL 2.1. See the enclosed
The files src/util/{i} are derived from the sources of OCaml
3.12 standard library, and are distributed under the GNU LGPL version
xx (see file OCAML-LICENSE).
See the enclosed file INSTALL.
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment