Editing ACL2

{{Short description|Programming language and theorem prover}}
{{Infobox programming language
| bodystyle = width:320px
| logo = ACL2 Logo 2014 transparent.png
| name = ACL2
| paradigm = [[Functional programming|Functional]], [[metaprogramming|meta]]
| designer = [[Robert S. Boyer]], [[J Strother Moore]] and [[Matt Kaufmann]]
| developer = [[Matt Kaufmann]] and [[J Strother Moore]]
| year = 1990<ref>{{Cite web|url=https://www.cs.utexas.edu/users/moore/acl2/current/manual/index.html?topic=ACL2____NOTE-1-7|title=XDOC — Note-1-7|website=www.cs.utexas.edu}}</ref> (limited distribution), 1996 (public distribution)
| latest_release_version = 8.6
| latest_release_date = {{release_date|2024|10}}
| typing = [[Dynamic typing|Dynamic]]
| influenced_by = [[Common Lisp]], [[Nqthm]]
| license = [[BSD licenses|BSD]]
| website = {{url|http://www.cs.utexas.edu/users/moore/acl2}}
| operating_system = [[Cross-platform software|Cross-platform]]
}}

'''ACL2''' ('''A Computational Logic for Applicative Common Lisp''') is a [[software]] system consisting of a [[programming language]], an extensible theory in a [[first-order logic]], and an [[automated theorem prover]]. ACL2 is designed to support [[automated reasoning]] in inductive logical theories, mostly for software and [[hardware verification]]. The input language and implementation of ACL2 are written in [[Common Lisp]]. ACL2 is [[free and open-source software]].

==Overview==
The ACL2 programming language is an [[applicative programming language|applicative]] ([[Side-effect (computer science)|side-effect]] free) variant of Common Lisp.  ACL2 is untyped. All ACL2 [[Subroutine|functions]] are [[Total function|total]]&nbsp;— that is, every function maps each object in the ACL2 [[Universe (mathematics)|universe]] to another object in its universe.

ACL2's base theory [[axiom]]atizes the [[semantics]] 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 [[Consistency proof|logical consistency]].

The core of ACL2's theorem prover is based on [[term rewriting]], and this core is extensible in that user-discovered [[theorem]]s can be used as ad hoc [[Mathematical proof|proof]] techniques for subsequent [[conjecture]]s.

ACL2 is intended to be an "industrial strength" version of the Boyer–Moore theorem prover, [[Nqthm|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 [[Compiler|compiled]] and run [[native code|natively]].

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."<ref>{{Cite web|url=http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm|title=ACM: Press Release, March 15, 2006|date=August 1, 2008|archive-url=https://web.archive.org/web/20080801092315/http://campus.acm.org/public/pressroom/press_releases/3_2006/software.cfm |archive-date=2008-08-01 }}</ref><ref name=acmaward>{{cite web|publisher=[[Association for Computing Machinery]] |url=http://awards.acm.org/homepage.cfm?srt=all&awd=149 |work=ACM Awards |title=Software System Award |access-date={{Format date|2012|1|14}} |url-status=dead |archive-url=https://web.archive.org/web/20120402203501/http://awards.acm.org/homepage.cfm?srt=all&awd=149 |archive-date=2012-04-02 }}</ref>

==Proofs==

ACL2 has had numerous industrial applications.<ref>{{Cite web|url=http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html|title=ACL2 Annotated Bibliography|website=www.cs.utexas.edu}}</ref><ref>{{Cite web|url=https://www.cs.utexas.edu/users/moore/acl2/workshops.html|title=ACL2 Workshops and UT ACL2 Seminar|website=www.cs.utexas.edu}}</ref> 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]].<ref>{{cite journal | citeseerx = 10.1.1.43.3309 | title = A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm | journal = IEEE Transactions on Computers | year = 1996 | volume = 47 | last1 = Moore | first1 = J. Strother | last2 = Lynch | first2 = Tom | last3 = Kaufmann | first3 = Matt }}</ref>

Industrial users of ACL2 include AMD, Arm, Centaur Technology, IBM, Intel, Oracle, and Collins Aerospace.

==See also==
*[[List of proof assistants]]

==References==
{{reflist}}

==External links==
*[http://www.cs.utexas.edu/users/moore/acl2/ ACL2 website]
*[http://acl2s.ccs.neu.edu/ ACL2s - ACL2 Sedan - An Eclipse-based interface developed by Peter Dillinger and Pete Manolios that includes powerful features to provide users with more automation and support for specifying conjectures and proving theorems with ACL2.]

{{DEFAULTSORT:Acl2}}
[[Category:Lisp (programming language)]]
[[Category:Common Lisp (programming language) software]]
[[Category:Proof assistants]]
[[Category:Free theorem provers]]
[[Category:Lisp programming language family]]
[[Category:Software using the BSD license]]