EVES: Documentation
To use EVES, the following documentation will be of help.
 Reference Manual for the Language Verdi:. The reference
manual is the definitive (informal) document on Verdi and
discusses all the capabilities of the system. Note, the document
is a reference manual, not a users' guide. Pedagogical material
is sparse and primarily left to an appendix of examples.
Available in
DVI
and PostScript.
 The EVES Library: This document presents a library of
reusable mathematical concepts and was initially based on
Spivey's Z Mathematical Toolkit. This document is a source of
many useful mathematical concepts that can be used in your
models and specifications. Available in
DVI
and PostScript.
The above two documents use the Verdi syntax. The Reference
Manual is also available using the sVerdi syntax. Available in
DVI
and PostScript.
A tutorial on EVES using sVerdi is available in
DVI
and PostScript.
For an example of installing EVES, see the "Software manual
for Windows EVES Version 3.0." Available in
DVI
and PostScript.
Other reports of note include papers on the mathematical
semantics of EVES (A Formal Description of Verdi [DVI,
PostScript]
and an Alternative Semantics for Verdi [DVI,
PostScript],
a paper on the EVES proof logging facility (EVES Proof Checking
and Browsing: Final Report [DVI,
PostScript],
and papers on the rigorous development of the SPARC Verdi compiler
(Structure of the SPARC Verdi Compiler [DVI,
PostScript]
and A fourphase translation from Verdi to Intermediate Language [DVI,
PostScript]).
Though other example uses of EVES are included in the ORA
Canada Bibliography, we note the use of EVES to analyze
authentication protocols [DVI,
PostScript]
and the design of a oneway link [DVI,
PostScript].
All files have been compressed with UNIX compress.
