ACL2 Materials by Inmaculada Medina Bulo and Francisco Palomo Lozano

• "La Lógica Computacional ACL2 Programación y Razonamiento Automático":
  Notes in Spanish by Inmaculada Medina Bulo and Francisco Palomo Lozano
  • Introduction in English
    This handout approaches ACL2 from three different viewpoints: as a pure functional programming language, as a computational logic, and as an automated reasoning system. In order to illustrate several aspects of ACL2, basic operations on sorted number lists are implemented and some important properties about them are formally verified. Finally, the implementation is generalized with the formalization of strict weak orderings to replace the standard numerical order in list operations. Strict weak orderings represent a basic concept in the C++ Standard Template Library.
  • Introduction in Spanish
    Estos apuntes se acercan a ACL2 desde tres puntos de vista distintos: como un lenguaje de programación funcional puro, como una lógica computacional y como un sistema de razonamiento automatizado. Para ilustrar distintos aspectos de ACL2, se implementan operaciones básicas sobre listas numéricas ordenadas y se verifican formalmente algunas propiedades importantes sobre ellas. Finalmente, la implementación se generaliza con la formalización de órdenes estrictos débiles para remplazar el orden numérico habitual en las operaciones sobre listas. Los órdenes estrictos débiles representan un concepto básico en la Biblioteca Estándar de Plantillas de C++.
• "Software Verification with ACL2":
  Slides by Francisco Palomo Lozano
  • Introduction in English
    This presentation supports a gentle introduction to software verification with ACL2 from a programmer's perspective. It reviews examples of industrial applications of ACL2, provides links to installation instructions, and discusses the basic management of an ACL2 session, function definition and specification of the expected properties. Finally, a classroom case study is introduced, developing a sorting algorithm from scratch and refining it to a parallel version. During this process several aspects of correctness are brought into attention.
  • Introduction in Spanish
    Esta presentación sirve de apoyo para una introducción sencilla a la verificación de software con ACL2 desde la perspectiva de un programador. Repasa ejemplos de aplicaciones industriales de ACL2, proporciona enlaces a las instrucciones de instalación y discute el manejo básico de una sesión en ACL2, la definición de funciones y la especificación de las propiedades esperadas. Por último, presenta un ejemplo de clase en el que se desarrolla un algoritmo de ordenación desde el principio y se refina para obtener una versión paralela. A lo largo de este proceso se traen a colación distintos aspectos de la corrección.