why.1 565 Bytes
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39
.TH why 1 "February, 2010"

.SH NAME
why \- A language for program verification


.SH SYNOPSIS
.B why
[
.B options
]
.B files


.SH DESCRIPTION

.B why
is a verification tool. 
It takes annotated programs as input 
and outputs verification conditions for several proof assistants (Coq,
PVS, Isabelle/HOL, etc.) and decision procedures (Alt-Ergo, Simplify,
Z3, etc.).

.SH OPTIONS

.TP
.B \-h
Help. Will give you the full list of command line options.


.SH CONTACT
.I Jean-Christophe Filliatre <filliatr@lri.fr>


.SH SEE ALSO

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