[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

ProofLite Package for PVS 3.1

Announcement: ProofLite Package for PVS 3.1
ProofLite is a library package for non-interactive proof scripting in
PVS. It allows for a literary proving style in PVS where specification
and proof scripts reside in the same file (as it is done in Coq and
other proof assistants). ProofLite is also suitable for automatic or
batch generation of specifications and proof scripts.

PVSio is freely available at:

We welcome comments and user reports,
Cesar Munoz

Cesar A. Munoz H., Senior Staff Scientist     mailto:munoz@nianet.org
National Institute of Aerospace      mailto://C.A.Munoz@larc.nasa.gov
144 Research Drive                  http://research.nianet.org/~munoz
Hampton, VA 23666, USA   Tel. +1 (757) 766 1539 Fax +1 (757) 766 1855