The books in this directory demonstrate a proof of correctness of
a BDD manager written with stobjs in ACL2.

Gzipped tar file: bdds.tar.gz

BOOK descriptions
-----------------
bdd-mgr.lisp  -- definition of bdd-mgr operations and guard proofs
bdd-spec.lisp -- definition of specification bdd function (no stobjs)
                 and various proofs about bdd algorithms in general
bdd-prf.lisp  -- proof that the bdd-mgr functions implement the bdd-spec
                 functions and that a satisfiability checker defined
                 with the bdd-mgr operations is correct

To build the books in this directory (in the correct order),
perform the following commands:

<shell> ACL2
<lisp>  (lp)
ACL2 !> (ld "make.lisp")


   -Rob Sumners
    robert.sumners@amd.com