World Library  
Flag as Inappropriate
Email this Article


Paradigm Functional, Metaprogramming
Designed by Robert S. Boyer, J Strother Moore and Matt Kaufmann
Developer Matt Kaufmann and J Strother Moore
First appeared 1990 (limited distribution), 1996 (public distribution)
Stable release 7.1 / May 2015 (2015-05)
Typing discipline dynamic
OS Cross-platform
License BSD 3-clause license
Website //acl2/moore/
Influenced by
Nqthm (theorem prover), Common Lisp

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 a mechanical theorem 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 on Common Lisp. ACL2 is free, open source (BSD license) software.

The ACL2 programming language is an applicative (side-effect free) variant of Common Lisp. ACL2 is untyped. 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 axiomatizes 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 logical consistency.

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

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, 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."[1][2]


ACL2 has had numerous industrial applications.[3][4] 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.[5] The interesting applications page of the ACL2 documentation has a summary of some uses of the system.

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


  1. ^ ACM: Press Release, March 15, 2006
  2. ^ "Software System Award". ACM Awards.  
  3. ^ Books and Papers about ACL2 and Its Applications
  4. ^ The ACL2 Workshop Series
  5. ^ "A mechanically checked proof of the correctness of the kernel of the AMD5K86 floating point division algorithm".  

External links

  • ACL2 website
  • 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.
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.
Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.
By using this site, you agree to the Terms of Use and Privacy Policy. World Heritage Encyclopedia™ is a registered trademark of the World Public Library Association, a non-profit organization.

Copyright © World Library Foundation. All rights reserved. eBooks from Project Gutenberg are sponsored by the World Library Foundation,
a 501c(4) Member's Support Non-Profit Organization, and is NOT affiliated with any governmental agency or department.