Dracula: A Guide to ACL2 in DrScheme

This manual provides an introduction to Dracula, the programming environment for the ACL2 theorem prover in DrScheme. See section 1 for instructions on installing, upgrading, and uninstalling Dracula. See section 2 for a tutorial on running and verifying programs using Dracula and ACL2. Section 3 introduces DoubleCheck, the teachpack for using automated testing to check your conjectures. Section 4 introduces Modular ACL2, an extension of ACL2 that supports systematic, piece-by-piece development and verification of ACL2 proofs.

See Dracula: Reference Manual for a full description of Dracula’s languages and libraries in detail, or the ACL2 home page for more information on the ACL2 theorem prover.