ACL2

ACL2

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 (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 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, 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 the AMD K5 microprocessor in the wake of the Pentium FDIV bug.

External links

* [http://www.cs.utexas.edu/users/moore/acl2/ ACL2 website]

References


Wikimedia Foundation. 2010.

Игры ⚽ Нужен реферат?

Look at other dictionaries:

  • ACL2 — es, a la vez, un lenguaje de programación, una lógica matemática para especificar y demostrar formalmente propiedades de los programas escritos en dicho lenguaje, y un demostrador automático de teoremas que asiste al usuario en dicha tarea. ACL2… …   Wikipedia Español

  • ACL2 — es un demostrador automatizado de teoremas con una lógica basada en un subconjunto aplicativo del lenguaje Common Lisp. También está escrito es ese mismo sublenguaje y puede correr en diversas implementaciones de Common Lisp. Tiene un alto grado… …   Enciclopedia Universal

  • McCarthy 91 function — The McCarthy 91 function is a recursive function, defined by computer scientist John McCarthy as a test case for formal verification within computer science. The McCarthy 91 function is defined as The results of evaluating the function are given… …   Wikipedia

  • Check Wikipedia — Wikiproyecto:Check Wikipedia Saltar a navegación, búsqueda Esta página contiene de forma consciente fallos ortográficos. Los bots no deben intentar corregirlos. Atajo PR:CWPR:CW …   Wikipedia Español

  • Common Lisp — Paradigm(s) Multi paradigm: procedural, functional, object oriented, meta, reflective, generic Appeared in 1984, 1994 for ANSI Common Lisp Developer ANSI X3J13 committee Typing discipline …   Wikipedia

  • List of computer scientists — Expand list|date=August 2008This is a list of well known computer scientists, people who do work in computer science, in particular researchers and authors.Some persons notable as programmers are included here because they work in research as… …   Wikipedia

  • J Strother Moore — (his first name is the alphabetic character J ndash; not an abbreviated J. ) is a computer scientist, and he is a co developer of the Boyer Moore string search algorithm and the Boyer Moore automated theorem prover, Nqthm. A good example of the… …   Wikipedia

  • Renault Primaquatre — Infobox Automobile name = Renault Primaquatre stablemates = aka = Renault Type KZ manufacturer = Renault parent company = production = 1931 1941 predecessor = Renault KZ successor = Renault Colorale class = Mid size car Large Family Car platform …   Wikipedia

  • Lisp — Información general Paradigma multiparadigma: orientado a objetos, funcional, declarativo Apareció en 1958 Diseñado por John McCarthy …   Wikipedia Español

  • GNU Common Lisp — Тип Интерпретатор и компилятор Разработчик Проект GNU Написана на Си и Лисп Операционная система Unix подобные операционные системы, Microsoft Windows Последняя версия …   Википедия

Share the article and excerpts

Direct link
… Do a right-click on the link above
and select “Copy Link”