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 also uses the "defsystem.lisp" package due to Mark Kantrowitz
of CMU, to which the following notice applies:

     Use and copying of this software and preparation of derivative works
     based upon this software are permitted, so long as the following
     conditions are met:
	  o no fees or compensation are charged for use, copies, or
	    access to this software
	  o this copyright notice is included intact.
     This software is made available AS IS, and no warranty is made about 
     the software or its performance. 

This software also uses "b64.c" due to Bob Trower, to which the following
notice applies:

     Permission is hereby granted, free of charge, to any person
     obtaining a copy of this software and associated
     documentation files (the "Software"), to deal in the
     Software without restriction, including without limitation
     the rights to use, copy, modify, merge, publish, distribute,
     sublicense, and/or sell copies of the Software, and to
     permit persons to whom the Software is furnished to do so,
     subject to the following conditions:

     The above copyright notice and this permission notice shall
     be included in all copies or substantial portions of the
     Software.

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> ...