License:

The source files for Ever are copyrighted by Alan J. Hu in the
years indicated in the respective source files.  Permission is granted
to use, copy, modify, sell and/or distribute this software and its
documentation for any purpose without royalty, subject to the following
terms and conditions:

1.  The copyright and permission notices appear in all copies of the
software and related documentation.

2.  This software may not be called "Ever" if it has been modified
in any way, without the specific prior written permission of Alan J. Hu.

3.  THE SOFTWARE IS PROVIDED "AS-IS".  NO REPRESENTATIONS OR WARRANTIES
OF MERCHANTABILITY OR FITNESS FOR ANY PARTICULAR PURPOSE OR THAT THE
USE OF THE SOFTWARE WILL NOT INFRINGE ANY PATENTS, COPYRIGHTS, TRADEMARKS,
OR OTHER RIGHTS IS EXPRESSED OR IMPLIED.  ALAN J. HU, STANFORD UNIVERSITY,
AND THE UNIVERSITY OF BRITISH COLUMBIA SHALL NOT BE LIABLE FOR ANY
LIABILITY OR DAMAGES ARISING FROM THE USE OF THIS SOFTWARE.

Notes:

Ever was intended to be a testbed for research ideas, never as production
quality code.  While you *might* be able to use it to find bugs in complicated
systems, it is completely unsuitable for attempting to prove the correctness
of anything.  Accordingly, you agree to hold me (Alan Hu), the University of
British Columbia, and Stanford University harmless for any damages resulting
from the use of this code.

I apologize that the code is so ugly.  I have long promised to release the
code, and I have never had time to clean it up.  I hope that people find it
useful -- both as a source of ideas and as a vehicle for verification research.

There is no good documentation for Ever.  My PhD thesis at Stanford contains
an appendix describing the verifier.  The algorithms are described there
as well as in several papers.  All of these sources are available from my
web page at http://www.cs.ubc.ca/spider/ajh/index.html.  If all else fails,
you can always read the YACC grammar. :-)

Installation:

Ever requires David Long's BDD package, which is currently available via
the web from http://www-2.cs.cmu.edu/~modelcheck/bdd.html.  You should
get that first and build it.

The supplied Ever files assume that you've put the BDD and memory package
header files in the current directory, as well as the built libraries.
If you did a proper installation instead, you'll need to edit the makefile
as well as several #include paths.

Please let me know if you find any major bugs, or if you find Ever particularly
fun and/or useful.  Good luck, and happy hacking!

					--Alan J. Hu
					  ajh@cs.ubc.ca
					  September 14, 1997