ACL2 ( A Computational Logic for Applicative Common Lisp ) es un sistema de software que consta de un lenguaje de programación , una teoría extensible en lógica de primer orden y un demostrador automático de teoremas . ACL2 está diseñado para admitir el razonamiento automatizado en teorías lógicas inductivas, principalmente para la verificación de software y hardware . El lenguaje de entrada y la implementación de ACL2 están escritos en Common Lisp . ACL2 es un software libre y de código abierto .
El lenguaje de programación ACL2 es una variante aplicativa ( sin efectos secundarios ) de Common Lisp. ACL2 no tiene tipos. Todas las funciones de ACL2 son totales , es decir, cada función asigna cada objeto del universo ACL2 a otro objeto de su universo.
La teoría básica de ACL2 axiomatiza la semántica de su lenguaje de programación y sus funciones integradas. Las definiciones de usuario en el lenguaje de programación que satisfacen un principio de definición extienden la teoría de una manera que mantiene la coherencia lógica de la teoría .
El núcleo del demostrador de teoremas de ACL2 se basa en la reescritura de términos , y este núcleo es extensible en el sentido de que los teoremas descubiertos por el usuario se pueden utilizar como técnicas de prueba ad hoc para conjeturas posteriores .
ACL2 está pensado para ser una versión "de nivel industrial" del demostrador de teoremas de Boyer-Moore, NQTHM . Con este objetivo, ACL2 tiene muchas características que respaldan la ingeniería limpia de teorías matemáticas y computacionales interesantes. ACL2 también obtiene eficiencia al estar construido sobre Common Lisp; por ejemplo, la misma especificación que es la base para la verificación inductiva se puede compilar y ejecutar de forma nativa .
En 2005, los autores de la familia de probadores Boyer-Moore, que incluye ACL2, recibieron el premio ACM Software System Award "por ser pioneros y diseñar un probador de teoremas sumamente eficaz (...) como herramienta de métodos formales para verificar hardware y software críticos para la seguridad". [2] [3]
ACL2 ha tenido numerosas aplicaciones industriales. [4] [5] En 1995, J Strother Moore , Matt Kaufmann y Tom Lynch utilizaron ACL2 para demostrar la corrección de la operación de división de punto flotante del microprocesador AMD K5 a raíz del error FDIV de Pentium . [6]
Los usuarios industriales de ACL2 incluyen AMD, Arm, Centaur Technology, IBM, Intel, Oracle y Collins Aerospace.