- ACL2
ACL2, (A Computational Logic for Applicative Common Lisp), is a software system consisting of a
programming language , an extensible theory in afirst-order logic , and a mechanicaltheorem prover . ACL2 is designed to support automated reasoning in inductive logical theories, mostly for the purpose of software and hardware verification. The input language and implementation of ACL2 are built onCommon Lisp . ACL2 is free,open source (GPL) software.The ACL2 programming language is an applicative (side-effect free) variant of Common LISP. ACL2 is unityped. All ACL2 functions are total — that is, every function maps each object in the ACL2 universe to another object in its universe.
ACL2's base theory
axiom atizes thesemantics of its programming language and its built-in functions. User definitions in the programming language that satisfy a "definitional principle" extend the theory in a way that maintains the theory's logical consistency.The core of ACL2's theorem prover is based on
term rewriting , and this core is extensible in that user-discoveredtheorems can be used as ad-hoc proof techniques for subsequentconjectures .ACL2 is intended to be an "industrial strength" version of the Boyer-Moore theorem prover, NQTHM. Toward this goal, ACL2 has many features to support clean engineering of interesting mathematical and computational theories. ACL2 also derives efficiency from being built on Common LISP; for example, the same specification that is the basis for inductive verification can be
compiled and run natively.In 2005, ACL2, as part of the Boyer-Moore family of provers, received the ACM Software System Award "for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software." [ [http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm ACM: Press Release, March 15, 2006 ] ]
Proofs
Proofs developed using ACL2
*
J Strother Moore used ACL2 to prove the correctness of the floating point division operations of theAMD K5 microprocessor in the wake of thePentium FDIV bug .External links
* [http://www.cs.utexas.edu/users/moore/acl2/ ACL2 website]
References
Wikimedia Foundation. 2010.