 | |
| Paradigm | Functional,meta |
|---|---|
| Designed by | Robert S. Boyer,J Strother Moore andMatt Kaufmann |
| Developer | Matt Kaufmann andJ Strother Moore |
| First appeared | 1990[1] (limited distribution), 1996 (public distribution) |
| Stable release | 8.6 / October 2024 (2024-10) |
| Typing discipline | Dynamic |
| OS | Cross-platform |
| License | BSD |
| Website | www |
| Influenced by | |
| Common Lisp,Nqthm | |
ACL2 (A Computational Logic for Applicative Common Lisp) is asoftware system consisting of aprogramming language, an extensible theory in afirst-order logic, and anautomated theorem prover. ACL2 is designed to supportautomated reasoning in inductive logical theories, mostly for software andhardware verification. The input language and implementation of ACL2 are written inCommon Lisp. ACL2 isfree and open-source software.
The ACL2 programming language is anapplicative (side-effect free) variant of Common Lisp. ACL2 is untyped. All ACL2functions aretotal — that is, every function maps each object in the ACL2universe to another object in its universe.
ACL2's base theoryaxiomatizes thesemantics of its programming language and its built-in functions. User definitions in the programming language that satisfy adefinitional principle extend the theory in a way that maintains the theory'slogical consistency.
The core of ACL2's theorem prover is based onterm rewriting, and this core is extensible in that user-discoveredtheorems can be used as ad hocproof 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 becompiled and runnatively.
In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, received theACM Software System Award "for pioneering and engineering a most effective theorem prover (...) as a formal methods tool for verifying safety-critical hardware and software."[2][3]
ACL2 has had numerous industrial applications.[4][5] In 1995,J Strother Moore,Matt Kaufmann and Tom Lynch used ACL2 to prove the correctness of the floating point division operation of theAMD K5 microprocessor in the wake of thePentium FDIV bug.[6]
Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.