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