NAME¶

why - A multi-language multi-prover verification tool

SYNOPSIS¶

why [ options ] files

DESCRIPTION¶

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 <filliatr@lri.fr>

SEE ALSO¶

Why web site: http://why.lri.fr/