Teach Yourself Dracula ACL2

Goal

To provide you with step-by-step instructions to teach yourself how to verify programs using ACL2.

Prerequisites

The goal of this tutorial is to require very little from you.

The Steps

1. Read the tutorial.
2. Download DrScheme.
3. Download Dracula.
   • You can install Dracula by running

     planet -i cce dracula.plt 2 9 

     after installing DrScheme.
4. Download ACL2.
5. Try these exercises

References

1. Dracula, Carl Eastlund
2. ACL2, by J Moore and Matt Kaufmann.
3. Workshop on Teaching Program Correctness, organized by Rex Page

---

Access Permissions: (Please don't edit)

• Set ALLOWTOPICCHANGE = DraculaGroup