We illustrate the power of partial-encapsulate, showing how it is used in the implementation of floating-point operations in ACL2.

The experience of an ACL2 user generally includes many failed proof attempts. A key to successful use of the ACL2 prover is the effective use of tools to debug those failures. We focus on changes made after ACL2 Version 8.5: the improved break-rewrite utility and the new utility, with-brr-data.

VWSIM is a circuit simulator for rapid, single-flux, quantum (RSFQ) circuits. The simulator is designed to model and simulate primitive-circuit devices such as capacitors, inductors, Josephson Junctions, and can be extended to simulate other circuit families, such as CMOS. Circuit models can be provided in the native VWSIM netlist format or as SPICE-compatible netlists, which are flattened and transformed into symbolic equations that can be manipulated and simulated. Written in the ACL2 logic, VWSIM provides logical guarantees about each of the circuit models it simulates. Note, our matrix solving and evaluation routines use Common Lisp floating-point numbers, and work is ongoing to admit these models into ACL2. We currently use VWSIM to help us design self-timed, RSFQ-based circuits. Our eventual goal is to prove properties of RSFQ circuit models. The ACL2-based definition of the VWSIM simulator offers a path for specifying and verifying RSFQ circuit models.

This article describes how ACL2 mechanizes mathematical induction. The techniques, which involve three well-known mathematical ideas and a handful of heuristics, were first demonstrated in Boyer and Moore’s Edinburgh Pure Lisp Theorem Prover (PLTP) of 1973, which was the first prover to attempt to automate induction in a general setting [10, 1]. Logically, the method depends on well-founded relations over some domain, a principle of definition admitting recursively defined functions justified by decreasing measures ensuring termination, and a principle of induction that is the precise dual of the principle of definition. The heuristics create plausible inductions for a conjecture and help choose among them. The generality of the mathematical formalizations and of the heuristics were then elaborated, first in Boyer and Moore’s Thm and Nqthm provers [2, 3, 4] prover of the late 1970s and the 1980s and then in Kaufmann and Moore’s ACL2 [7, 9] which was started by Boyer and Moore in 1989 but has been under continuous development by Kaufmann and Moore since 1992. ACL2 is in regular industrial use today [15]. This article narrowly focuses on ACL2 but is not intended specifically for the ACL2 audience. For a much deeper and broader discussion of the history of the mechanization of explicit and implicit induction and various

We describe how we have defined in ACL2 a weak version of the Common Lisp functional apply, which takes a function and list of actuals and applies the function to the actuals. Our version, called apply$, does not operate on functions but on ordinary objects—symbols and lists representing lambda expressions—some of which are interpreted as functions. We define a syntactic notion of “tameness” to identify the interpretable objects. This makes our apply$ weaker than a true second-order functional but we believe apply$ is powerful enough for many uses in ACL2. To maintain soundness and the conservativity of our Definitional Principle we require that certain hypotheses, called “warrants”, be present in any theorem relying on the behavior of apply$ on non-primitives. Within these constraints we can define “functionals” such as sum and foldr which map tame “functions” over lists and accumulate the results. This allows the ACL2 user to avoid defining specialized recursive functions for each such application. We can prove and use general-purpose lemmas about these “functionals.” We describe the formalization, explain how we keep the Definitional Principle conservative, show examples of useful functions using apply$ and theorems about them, sketch the proof that there is a model of any extension of the system using the new primitives, discuss issues arising in making these functions executable, and show some preliminary performance results.

Iterative algorithms are traditionally expressed in ACL2 using recursion. On the other hand, Common Lisp provides a construct, loop, which -- like most programming languages -- provides direct support for iteration. We describe an ACL2 analogue loop$ of loop that supports efficient ACL2 programming and reasoning with iteration.

We discuss the evolutionary path from the Edinburgh Pure Lisp Theorem Prover of the early 1970s to its modern counterpart, AComputational Logic for Applicative Common Lisp, aka ACL2, which is in regular industrial use. Among the milestones in this evolution are the adoption of a first-order subset of a programming language as a logic; the analysis of recursive definitions to guess appropriate mathematical induction schemes; the use of simplification in inductive proofs; the incorporation of rewrite rules derived from user-suggested lemmas; the generalization of that idea to allow the user to affect other proof techniques soundly; the recognition that evaluation efficiency is paramount so that formal models can serve as prototypes and the logic can be used to reprogram the system; use of the system to prove extensions correct; the incorporation of decision procedures; the provision of hierarchically structured libraries of previously certified results to configure the prover; the provision of system programming features to allow verification tools to be built and verified within the system; the release of many verified collections of lemmas supporting floating point, programming languages, and hardware platforms; a verified “bit-bashing” tool exploiting verified BDD and checked external SAT procedures; and the provisionof certain higher-order features within the first-order setting. As will become apparent, some of these milestones were suggested or even prototyped by users. Some additional non-technical aspects of the project are also critical. Among these are a devotion to soundness, good documentation, freely available source code, production of a system usable by industry, responsiveness to user needs, and a dedicated, passionate, and brilliant user community.

Industrial applications of interactive theorem proving dates back to the eighties. Enabling and achieving industrial successes has been an important focus of the ACL2 community. The ARCADE call-for-papers appears to ignore these results and the potential of automated reasoning in industry in the future. We briefly describe the penetration of the ACL2 theorem proving system into the microprocessor industry, list some of milestones achieved, the obstacles standing in the way, and some future research directions.

The ACL2 theorem prover has seen sustained industrial use since the mid-1990s. Companies that have used ACL2 regularly include AMD, Centaur Technology, IBM, Intel, Kestrel Institute, Motorola/Freescale, Oracle and Rockwell Collins. This paper introduces ACL2 and focuses on how and why ACL2 is used in industry. ACL2 is well-suited to its industrial application to numerous software and hardware systems, because it is an integrated programming/proof environment supporting a subset of the ANSI standard Common Lisp programming language. As a programming language ACL2 permits the coding of efficient and robust programs; as a prover ACL2 can be fully automatic but provides many features permitting domain-specific human-supplied guidance at various levels of abstraction. ACL2 specifications and models often serve as efficient execution engines for the modelled artefacts while permitting formal analysis and proof of properties. Crucially, ACL2 also provides support for the development and verification of other formal analysis tools. However, ACL2 did not find its way into industrial use merely because of its technical features. The core ACL2 user/development community has a shared vision of making mechanized verification routine when appropriate and has been committed to this vision for the quarter century since the Computational Logic, Inc., Verified Stack. The community has focused on demonstrating the viability of the tool by taking on industrial projects (often at the expense of not being able to publish much).This article is part of the themed issue 'Verified trustworthy software systems'.

Industrial applications of interactive theorem proving dates back to the eighties. Enabling and achieving industrial successes has been an important focus of the ACL2 community. The ARCADE call-for-papers appears to ignore these results and the potential of automated reasoning in industry in the future. We briefly describe the penetration of the ACL2 theorem proving system into the microprocessor industry, list some of milestones achieved, the obstacles standing in the way, and some future research directions.

When operational semantics is used as the basis for mechanized verification of machine code programs it is often necessary for the theorem prover to determine whether one expression denoting a machine address is unequal to another. For example, this problem arises when trying to determine whether a read at the address given by expression a is affected by an earlier write at the address given by b. If it can be determined that a and b are definitely unequal, the write does not affect the read. Such address expressions are typically composed of “machine arithmetic function symbols” such as +, *, mod, ash, logand, logxor, etc., as well as numeric constants and values read from other addresses. In this chapter we present an abstract interpreter for machine address expressions that attempts to produce a bounded natural number interval guaranteed to contain the value of the expression. The interpreter has been proved correct by the ACL2 theorem prover and is one of several key technologies used to do fast symbolic execution of machine code programs with respect to a formal operational semantics. We discuss the interpreter, what has been proved about it by ACL2, and how it is used in symbolic reasoning about machine code.

Some runtime checks can be safely removed from code if appropriate program properties are proved. We describe how we have applied this idea to the ACL2 theorem prover to speed up the application of user-defined proof procedures. In particular, we discuss how and why we have added a new feature to ACL2 that allows the user to verify certain well-formedness properties of the expressions produced by user-defined proof procedures. Of special interest are the issues of extensibility (how we know that guarantees proved in one theory are adequate in another), formalization of the problem, and design

When ACL2 is used to model the operational semantics of computing machines, machine states are typically represented by terms recording the contents of the state components. When models are realistic and are stepped through thousands of machine cycles, these terms can grow quite large and the cost of simplifying them on each step grows. In this paper we describe an ACL2 book that uses HIDE and metafunctions to facilitate the management of large terms representing such states. Because the metafunctions for each state component updater are solely responsible for creating state expressions (i.e., "writing") and the metafunctions for each state component accessor are solely responsible for extracting values (i.e., "reading") from such state expressions, they can maintain their own normal form, use HIDE to prevent other parts of ACL2 from inspecting them, and use honsing to uniquely represent state expressions. The last feature makes it possible to memoize the metafunctions, which can improve proof performance in some machine models. This paper describes a general-purpose ACL2 book modeling a byte-addressed memory supporting "mixed" reads and writes. By "mixed" we mean that reads need not correspond (in address or number of bytes) with writes. Verified metafunctions simplify such "read-over-write" expressions while hiding the potentially large state expression. A key utility is a function that determines an upper bound on the value of a symbolic arithmetic expression, which plays a role in resolving writes to addresses given by symbolic expressions. We also report on a preliminary experiment with the book, which involves the production of states containing several million function calls.

Computer hardware and software can be modeled precisely in mathematical logic. If expressed appropriately, these models can be executable, i.e., run on concrete data. This allows them to be used as simulation engines or rapid prototypes. But because they are formal they can be manipulated by symbolic means: theorems can be proved about them, directly, with mechanical theorem provers. But how practical is this vision of machines reasoning about machines? In this highly personal talk, I will describe the 45 year history of the “Boyer-Moore theorem prover,” starting with its use in Edinburgh, Scotland, to prove simple list processing theorems by mathematical induction (e.g., the reverse of the reverse of x is x) to its routine commercial use in the microprocessor industry (e.g., the floating point operations of the Via Nano 64-bit X86 microprocessor are compliant with the IEEE standard). Along the way we will see applications in program verification, models of instruction set architectures including the JVM, and security and information flow. I then list some reasons this project has been successful. The paper also serves as an annotated bibliography of the key stepping stones in the applications of the prover.

We report on improvements to ACL2 made since the 2013 ACL2 Workshop.

In this paper we sketch an ACL2-checked proof that a simple but unbounded Von Neumann machine model is Turing Complete, i.e., can do anything a Turing machine can do. The project formally revisits the roots of computer science. It requires re-familiarizing oneself with the definitive model of computation from the 1930s, dealing with a simple "modern" machine model, thinking carefully about the formal statement of an important theorem and the specification of both total and partial programs, writing a verifying compiler, including implementing an X86-like call/return protocol and implementing computed jumps, codifying a code proof strategy, and a little "creative" reasoning about the non-termination of two machines.

Previous work by the authors generalized conditional rewrit- ing from the use of equalities to the use of arbitrary equivalence relations. This (classic) equivalence-based rewriting automates the replacement of one subterm by another that may not be strictly equal to it, but is equivalent to it, where this equivalence is determined automatically to be sufficient at that subterm occurrence. We extend that capability by introducing patterned congruence rules in the ACL2 theorem prover, to provide more control over the occurrences where such a replacement may be made. This extension enables additional automation of the rewriting process, which is important in industrial-scale applications. However, be- cause this feature is so new (introduced January, 2014), we do not yet have industrial applications to verify its utility, so we present a small example that illustrates how it supports scaling to large proof efforts.

Previous work by the authors generalized conditional rewriting from the use of equalities to the use of arbitrary equivalence relations. Such (classic) equivalence-based rewriting automates the replacement of one subterm by another that may not be strictly equal to it, but is equivalent to it, where this equivalence is determined automatically to be sufficient at that subterm occurrence. We extend that capability by introducing patterned congruence rules in the ACL2 theorem prover, to provide more control over the occurrences where such a replacement may be made. This extension enables additional automation of the rewriting process, which is important in industrial-scale applications. However, because this feature is so new (introduced January, 2014), we do not yet have industrial applications to verify its utility, so we present a small example that illustrates how it supports scaling to large proof efforts.