Package why3

Software verification platform

Why3 is the next generation of the Why software verification platform.
Why3 clearly separates the purely logical specification part from
generation of verification conditions for programs. It features a rich
library of proof task transformations that can be chained to produce a
suitable input for a large set of theorem provers, including SMT
solvers, TPTP provers, as well as interactive proof assistants.

General Commands (Section 1)
Verify conditions in source code. If the filename is "-", then input is read from stdin.
The why3bench tool adds a scheduler on top of the Why3 library. It is designed to compare various components of automatic proofs: automatic provers...
Why3 must be configured to access external provers. Typically, this is done by either running this tool or using the menu File/Detect provers of the IDE. This...
Run a command with CPU and virtual memory limits. One of -h or -s must be specified. TIME specifies the maximum runtime in seconds. MEMORY specifies the maximum...
Format Why3 theories in HTML for human viewing.
Start the Why3 IDE, either loading an initial file, or starting in a given project directory.
This tool is an additional layer on top of the Why3 library for generating verification conditions from Why3ML programs. It accepts the same command line...
Produce a realization of a Why3 theory.
The purpose of the why3replayer tool is to execute the proofs stored in a Why3 session file, such as the one produced by the IDE. Its main goal is to play...