ACL2 Workshop 2023
Abstracts

I will give an overview of Kestrel Institute's Axe toolkit, which I have been developing for over 15 years. Axe is based on ACL2 and contains a variety of high-performance formal verification tools, including rewriters, provers, equivalence checkers, testers, and lifters from low-level languages such as JVM bytecode and x86 machine code. Axe has been used to verify and analyze a variety of programs, especially cryptographic algorithms. Key to Axe's performance is its representation of terms as directed acyclic graphs, with maximal structure sharing. Axe is implemented as an ACL2 program and increasingly consists of logic-mode guard-verified code.

I will also discuss the libraries that I have developed to support Axe and some lessons learned along the way about effective use of ACL2.

Jim has spent 25 years in industry developing and applying formal verification tools, and managing formal verification projects in domains where the application of formal is driven by business imperatives rather than curiosity or regulatory requirement. This talk will present some collected lessons on where to apply formal verification and how to position formal verification projects for success.

[Slides]

We show how equivalence relations can be used to capture a function's define/use behaviors and how congruences can then be used to automate certain common simplifications.

[Slides]

This talk will present work in progress towards adding support for floating-point computations in ACL2. Semantically, floating-point operations in ACL2 are to be partially constrained operations on certain rational numbers: those that are representable as double-precision floating point numbers. Yet, fast floating-point execution is to be supported by way of syntax checking similar to what is done for single-threaded objects (stobjs). Examples will be presented based on a preliminary implementation.

[Talk notes]

Note: See also :DOC topic, INDUCTION-COARSE-V-FINE-GRAINED.

Sometimes a function can be admitted under the default ruler-extenders but inductive proofs about the function seem excessively long. This is especially true for functions that contain LET and LET* expressions in which local variables are bound to IF expressions containing recursive calls. (That style is often useful because it facilitates code sharing.) We've found that changing ruler-extenders to produce a finer case analysis, while often not necessary for admission, produces an induction scheme that is more suitable. In this talk I'll show an example.

This talk on "Formalizing 100 Theorems" (see http://www.cs.ru.nl/~freek/100/) will have 2 purposes: (1) to report on our progress (40-some theorems proved with ACL2 or Nqthm) and (2) to encourage contributions from others.

[Slides]

Our goal to boot Linux on the ACL2 x86-ISA model has been reached. This effort was started in ~2004 with Hunt developing a litany of y86 models in support of Bryant and O'Hallaron architecture book series. Early last decade, Hunt started an effort to model the x86-ISA. In 2012, Hunt and Kaufmann produced an early ACL2 64-bit x86-ISA model, which then was replaced by a litany of increasingly more accurate and complete models. As a part of Shilpi Goel's PhD work, she extended the ACL2 x86-ISA model significantly. Cuong Chau added definitions for floating-point operations and Alessandro Coglio added support for 32-bit x86-ISA instructions. Over the last six months, we extended and corrected the ACL2 x86-ISA model so it can boot Linux and run user programs. Much work remains, as our device complement is limited to a console and a crude timer; our effort does include file-system (block I/O) support, but lacks network support.

[Slides]

I will present our work on DARPA PEARLS, in which the Kestrel team built ML models and heuristics to find and repair ACL2 proofs (e.g., suggesting hints, libraries, hypotheses, etc.). I will also discuss some related tools that are of more general interest, including a tool that suggests improvements to ACL2 books.