= ACL2 =

[http://www.cs.utexas.edu/users/moore/acl2/ ACL2] is a modeling and analysis tool, which is regularly used to help ensure the correctness and security of computing system.

The '''ACL2''' system is written in Common Lisp, and '''OpenMCL''' is used for '''ACL2''' development and deployment. Enhancements and extensions so OpenMCL will better support analysis and theorem proving is being funded, in part, by [http://en.wikipedia.org/wiki/DARPA DARPA] and the [http://www.nsf.gov/ NSF] under subcontract from the [http://www.utexas.edu/ University of Texas].

Please contact Professor Warren A. Hunt, Jr., [mailto:hunt@cs.utexas.edu <hunt@cs.utexas.edu>], for additional information.