ACL2
Developer Matt Kaufmann and J Strother Moore | | |
| First appeared | 1990[1] (limited distribution), 1996 (public distribution) | |
|---|---|---|
| Stable release | 8.5
/ July 2022 | |
Dynamic | ||
| OS | Cross-platform | |
| License | BSD | |
| Website | www | |
| Influenced by | ||
| Common Lisp, Nqthm | ||
ACL2 (A Computational Logic for Applicative Common Lisp) is a
Overview
The ACL2 programming language is an
ACL2's base theory
The core of ACL2's theorem prover is based on
ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover,
In 2005, the authors of the Boyer-Moore family of provers, which includes ACL2, 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."[2][3]
Proofs
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 the AMD K5 microprocessor in the wake of the Pentium FDIV bug.[6] The interesting applications page of the ACL2 documentation has a summary of some uses of the system.
Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.
See also
- List of proof assistants
References
- ^ "XDOC — Note-1-7". www.cs.utexas.edu.
- ^ "ACM: Press Release, March 15, 2006". August 1, 2008. Archived from the original on 2008-08-01.
- ^ "Software System Award". ACM Awards. Association for Computing Machinery. Archived from the original on 2012-04-02. Retrieved January 14, 2012.
- ^ "ACL2 Annotated Bibliography". www.cs.utexas.edu.
- ^ "ACL2 Workshops and UT ACL2 Seminar". www.cs.utexas.edu.
- CiteSeerX 10.1.1.43.3309.