 | |
| Paradigma | Funcional , meta |
|---|---|
| Diseñada por | Robert S. Boyer , J Strother Moore y Matt Kaufmann |
| Desarrollador | Matt Kaufmann y J Strother Moore |
| Apareció por primera vez | 1990 (distribución limitada), 1996 (distribución pública) |
| Lanzamiento estable | 8.2 / mayo de 2019 |
| Disciplina de mecanografía | Dinámica |
| SO | Multiplataforma |
| Licencia | BSD |
| Sitio web | www |
| Influenciado por | |
| Lisp común , Nqthm | |
ACL2 ("Una lógica computacional para Common Lisp aplicativo") es un sistema de software que consta de un lenguaje de programación , una teoría extensible en una lógica de primer orden y un demostrador de teoremas automatizado . ACL2 está diseñado para respaldar el razonamiento automatizado en teorías lógicas inductivas, principalmente con el propósito de 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 gratuito y de código abierto .
Resumen [ editar ]
El lenguaje de programación ACL2 es una variante aplicativa ( sin efectos secundarios ) de Common Lisp. ACL2 no tiene tipo. Todas las funciones de ACL2 son totales , es decir, cada función asigna cada objeto del universo de 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 amplían la teoría de una manera que mantiene la consistencia 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á destinado a ser una versión de "fuerza industrial" del demostrador del teorema de Boyer-Moore, NQTHM . Con este objetivo, ACL2 tiene muchas características para respaldar 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 más efectivo (...) como una herramienta de métodos formales para verificar hardware crítico para la seguridad. y software ". [1] [2]
Pruebas [ editar ]
ACL2 ha tenido numerosas aplicaciones industriales. [3] [4] En 1995, J Strother Moore , Matt Kaufmann y Tom Lynch utilizaron ACL2 para probar la exactitud de la operación de división de punto flotante del microprocesador AMD K5 a raíz del error Pentium FDIV . [5] La página de aplicaciones interesantes de la documentación de ACL2 tiene un resumen de algunos usos del sistema.
Los usuarios industriales de ACL2 incluyen AMD, Arm, Centaur Technology, IBM, Intel, Oracle y Rockwell Collins.
Referencias [ editar ]
- ^ ACM: Comunicado de prensa, 15 de marzo de 2006
- ^ "Premio al sistema de software" . Premios ACM . Asociación de Maquinaria Informática . Archivado desde el original el 2 de abril de 2012 . Consultado el 14 de enero de 2012 .
- ^ Libros y artículos sobre ACL2 y sus aplicaciones
- ^ La serie de talleres ACL2
- ^ "Una prueba comprobada mecánicamente de la corrección del kernel del algoritmo de división de punto flotante AMD5K86". CiteSeerX 10.1.1.43.3309 . Cite journal requiere
|journal=( ayuda )
Enlaces externos [ editar ]
- Sitio web de ACL2
- ACL2s - ACL2 Sedan: una interfaz basada en Eclipse desarrollada por Peter Dillinger y Pete Manolios que incluye funciones poderosas para proporcionar a los usuarios más automatización y soporte para especificar conjeturas y demostrar teoremas con ACL2.
