carta
tool-stat(1)

tool-stat1

A multi-language multi-prover verification tool

Part of why(1).

Usage

why [options] files

Overview

why is a verification tool. It takes annotated programs as input (in ML or C syntax) and outputs verification conditions for several proof assistants (Coq, PVS, HOL Light, Mizar) and decision procedures (haRVey, Simplify).

Options

-h

Help. Will give you the full list of command line options.

Authors

Jean-Christophe Filliatre <[email protected]>

From why 2.34-2 in Debian 8 (Jessie). Parsed by carta from the page's man source.