NOTICES

PVS Specification and Verification System: NOTICES


This software uses, requires or incorporates, in whole or in part, the following
components, each of which is available as indicated and under the terms of the
GNU Public License (GPL).  A copy of the GPL is available in the file "LICENSE".

o Mona (Available from http://www.brics.dk/mona/)
o Emacs (Available from http://www.gnu.org/software/emacs/)

This software uses the following public domain software:

o md5.lisp (Pierre R. Mai)
o metering.lisp (Mark Kantrowitz, CMU)


SRI gratefully acknowledges the permission of the following entities and 
individuals for the use of their software, specification and proofs within 
PVS:

Frank Pfenning of CMU ("ERGO" system).
Cesar Munoz of NIA ("PVSio")
Geertleon Janssen ("BDD/MU Calculus")
C. Michael Holloway ("pvs-prover-helps.el")

... <add in acks to other folks for prelude things> ...