wiki:ACL2

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  DARPA and the  NSF under subcontract from the  University of Texas.

Please contact Professor Warren A. Hunt, Jr., , for additional information.