Package why3

Software verification platform

http://why3.lri.fr/

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)
why3
Verify conditions in source code. If the filename is "-", then input is read from stdin.
why3bench
The why3bench tool adds a scheduler on top of the Why3 library. It is designed to compare various components of automatic proofs: automatic provers...
why3config
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...
why3-cpulimit
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...
why3doc
Format Why3 theories in HTML for human viewing.
why3ide
Start the Why3 IDE, either loading an initial file, or starting in a given project directory.
why3ml
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...
why3realize
Produce a realization of a Why3 theory.
why3replayer
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...