The files in this directory contain the generic proofs of partial and total
correctness of sequential programs based on assertional reasoning, along with
demonstration programs, all in ACL2. The books associated are documented.
However, for a better and thorough understanding of how it all works, we
recommend reading the following paper:

J. Matthews, J S. Moore, S. Ray, and D. Vroon: "A Symbolic Simulation Approach
to Assertional Program Verification", Draft, 2005.

This paper is accessible on the web from either of the following URLs:

- http://www.cse.ogi.edu/~johnm/papers/MatthewsMooreRayVroon05.pdf
- http://www.cs.utexas.edu/users/sandip/publications/symbolic/main.html

The books are designed by the authors of the paper above, and contains valuable
enhancements and bug-fixes by Lee Pike. Lee Pike also contributed the triangle
example in the directory tiny-triangle.

To certify this set of books perform the following steps. 

(1) Fire up ACL2. 
(2) (ld "certify.lsp") at the ACL2 prompt.

Alternatively, you can run make.  If you want to do so in other than the
directory in which this is distributed, directly under the books/ directory of
the ACL2 distribution, you need to change the Makefile in each directory to
point to the appropriate Makefile-generic, and the Makefile in this directory
to point to the appropriate Makefile-subdirs.

For questions or comments on the ACL2 proofs, contact sandip@cs.utexas.edu.