
                    The Verus Model Checking System
                    ===============================


Verus is distributed under the license agreement below. Please sign
a copy of this agreement and return it to:

      Edmund Clarke
      School of Computer Science
      Carnegie Mellon University
      Pittsburgh, PA 15213-3890

We would request users of this software to return to

      Edmund Clarke                or  emc@CS.CMU.EDU
      School of Computer Science
      Carnegie Mellon University
      Pittsburgh PA 15213-3890

any material improvements or extensions to the Verus System and grant
Carnegie Mellon the rights to redistribute these changes subject to
the LICENSE AGREEMENT.

----------8<----------------------------------------------------------

Carnegie Mellon University (hereafter referred to as "LICENSOR")
agrees to provide to the person and/or institution signing this
document, hereinafter referred to as "LICENSEE", the following
software:
                 The Verus Model Checking System

hereinafter referred to as the "LICENSED SOFTWARE".

The LICENSOR hereby grants the LICENSEE a license to use and copy the
LICENSED SOFTWARE on or in connection with operation of any computer
system owned or operated by it. This license is subject to LICENSEE's
agreement to the following terms and conditions:

1. The LICENSEE acquires no ownership right, title, or interest in the
   LICENSED SOFTWARE materials provided by LICENSOR or any copyrights
   for the LICENSED SOFTWARE and documentation through this license.

1. LICENSEE agrees that any information, materials or services
   furnished by LICENSOR under this agreement are provided on an "as
   is" basis.  LICENSOR makes no warranties of any kind, either
   expressed or implied, as to any matter including, but not limited
   to, warranty of fitness of purpose, or merchantability, or results
   obtained from LICENSEE's use of the LICENSED SOFTWARE, nor shall
   either party hereto be liable to the other for indirect, special,
   or consequential damages such as loss of profits or inability to
   use the LICENSED SOFTWARE or any applications or derivations
   thereof.

2. The LICENSED SOFTWARE will not be transferred outside of the
   LICENSEE's institution and will be used only for research purposes.
   In particular, the LICENSEE agrees that the code will not be
   included as part of any commercial software package or product of
   this institution.

3. The LICENSEE will make no demands on the LICENSOR for maintenance
   and agrees that the LICENSOR has no obligation to provide any
   maintenance or consulting help with respect to the LICENSED
   SOFTWARE.

4. LICENSEE shall reproduce and include LICENSOR's copyright notice on
   any copies of the LICENSED SOFTWARE and applications and
   derivations thereof.



                   -----------------------------------------
                   <name and address>
