Rodney Martineau Burstall -Rod, as he was known to us all -died on Thursday, 13th February, 2025, after a long illness.Rod was a kind and generous man who will be remembered by those who knew him as much for his humanity as for his contributions to computer science.While he made major contributions to our subject, he constantly demonstrated humility, curiosity, openness, tolerance, and acceptance.He read widely and enjoyed discussing -or learning about -basically any topic that his conversational partner felt passionate about.Perhaps more than anything he exemplified a comfortable way of being human.To many of us that was his greatest contribution to our lives.Rod was born in 1934, the son of a draftsman and a housewife from Liverpool.He attended King George V Grammar School at Southport, moved on to King's College, Cambridge, reading Natural Sciences, and then took a Masters in

Abstract We discuss the evolutionary path from the Edinburgh Pure Lisp Theorem Prover of the early 1970s to its modern counterpart, A C omputational L ogic for A pplicative C ommon L isp, 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 provision of 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.

The ACL2 theorem prover---the current incarnation of "the" Boyer-Moore theorem prover---is a theorem prover for an extension of a first-order, applicative subset of Common Lisp. The ACL2 system provides a useful specification and modeling language as well as a useful mechanical theorem proving environment. ACL2 is in use at several major microprocessor manufacturers to verify functional correctness of important components of commercial designs. This talk explores the design of ACL2 and the tradeoffs that have turned out to be pivotal to its success.

Summary form only given. Since Turing, computer scientists have understood that the question "does this program satisfy its specifications?" could be reduced to the question "are these formulas theorems?" But the theorem proving technology of the 50s and 60s was inadequate for the task. In 1971, here in Edinburgh, Boyer and I started building the first general-purpose theorem prover designed for a computational logic. This project continues today, with Matt Kaufmann as a partner; the current version of the theorem prover is ACL2 (A Computational Logic for Applicative Common Lisp). In this talk I'll give a highly personal view of the four decade long "Boyer-Moore Project," including our mechanization of inductive proof, support for recursive definitions, rewriting with previously proved lemmas, integration of decision procedures, efficient representation of logical constants, fast execution, and other proof techniques. Along the way we'll see several interesting side roads: the founding of the Edinburgh school of logic programming, a structureshared text editor that played a role in the creation of Word, and perhaps most surprisingly, the use of our "Lisp theorem prover" to formalize and prove theorems about commercial microprocessors and virtual machines via deep embeddings, including parts of processors by AMD, Centaur, IBM, Motorola, Rockwell-Collins, Sun, and others. The entire project helps shed light on the dichotomy between general-purpose theorem pro vers and special-purpose analysis tools.

No abstract available.

Abstract We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.

Some functional programming languages are also mathematical logics. One can reason formally, traditionally, and directly about programs in such languages. This is driving a new application area for functional programming: modeling microarchitectures, hardware design languages, and imperative programming languages. Such models serve the dual purposes of simulation and formal analysis.ACL2, "A Computational Logic for Applicative Common Lisp," is a functional programming language that is also a first-order mathematical logic supported by a Boyer-Moore style mechanical theorem prover [5]. It is being used to model and verify artifacts of commercial and industrial interest.

We describe a mechanically checked proof of a property of a small system of Java programs involving an unbounded number of threads and synchronization, via monitors. We adopt the output of the javac compiler as the semantics and verify the system at the bytecode level under an operational semantics for the JVM. We assume a sequentially consistent memory model and atomicity at the bytecode level. Our operational semantics is expressed in ACL2, a Lisp-based logic of recursive functions. Our proofs are checked with the ACL2 theorem prover. The proof involves reasoning about arithmetic; infinite loops; the creation and modification of instance objects in the heap, including threads; the inheritance of fields from superclasses; pointer chasing and smashing; the invocation of instance methods (and the concomitant dynamic method resolution); use of the start method on thread objects; the use of monitors to attain synchronization between threads; and consideration of all possible interleavings (at the bytecode level) over an unbounded number of threads. Readers familiar with monitor-based proofs of mutual exclusion will recognize our proof as fairly classical. The novelty here comes from (i) the complexity of the individual operations on the abstract machine; (ii) the dependencies between Java threads, heap objects, and synchronization; (iii) the bytecode-level interleaving; (iv) the unbounded number of threads; (v) the presence in the heap of incompletely initialized threads and other objects; and (vi) the proof engineering permitting automatic mechanical verification of code-level theorems. We discuss these issues. The problem posed here is also put forth as a benchmark against which to measure other approaches to formally proving properties of multithreaded Java programs.

We report on the successful application of a mechanical theorem prover to the problem of verifying the division microcode program used on the AMD5/sub K/86 microprocessor. The division algorithm is an iterative shift and subtract type. It was implemented using floating point microcode instructions. As a consequence, the floating quotient digits have data dependent precision. This breaks the constraints of conventional SRT division theory. Hence, an important question was whether the algorithm still provided perfectly rounded results at 24, 53, or 64 bits. The mechanically checked proof of this assertion is the central topic of the paper. The proof was constructed in three steps. First, the divide microcode was translated into a formal intermediate language. Then, a manually created proof was transliterated into a series of formal assertions in the ACL2 dialect. After many expansions and modifications to the original proof, the theorem prover certified the assertion that the quotient will always be correctly rounded to the target precision.

ACL2 is a reimplemented extended version of R.S. Boyer and J.S. Moore's (1979; 1988) Nqthm and M. Kaufmann's (1988) Pc-Nqthm, intended for large scale verification projects. The paper deals primarily with how we scaled up Nqthm's logic to an industrial strength" programming language-namely, a large applicative subset of Common Lisp-while preserving the use of total functions within the logic. This makes it possible to run formal models efficiently while keeping the logic simple. We enumerate many other important features of ACL2 and we briefly summarize two industrial applications: a model of the Motorola CAP digital signal processing chip and the proof of the correctness of the kernel of the floating point division algorithm on the AMD5/sub K/86 microprocessor by Advanced Micro Devices, Inc.

Abstract We present a formal model of asynchronous communication between two digital hardware devices. The model takes the form of a function in the Boyer-Moore logic. The function transforms the signal stream generated by one processor into that consumed by an independently clocked processor, given the phases and rates of the two clocks and the communications delay. The model can be used quantitatively to derive concrete performance bounds on communications at ISO protocol level 1 (physical level). We use the model to show that an 18-bit/cell biphase mark protocol reliably sends messages of arbitrary length between two processors provided the ratio of the clock rates is within 5% of unity.

A proof by a computer program of the unsolvability of the halting problem is described.The halting problem is posed in a construcUve, formal language.The computational paradigm formalized ~s Pure LISP, not Tunng machines.The machine was led to the proof by the authors, who suggested certain function definitions and stated certain intermediate lemmas.The machine checked to ascertain that every suggested definition was admissible and the machine proved the main theorem and every lemma.It is beheved this is the first instance of a machine checking that a given problem is not solvable by machine.

We describe how to transform certain flowchart programs into equivalent explicit primitive recursive programs. The input/output correctness conditions for the transformed programs are more amenable to proof than the verification conditions for the corresponding flowchart programs. In particular, the transformed correctness conditions can often be verified automatically by the theorem prover developed by Boyer and Moore [1].

Program verification is the 1den that propertms of programs can be precisely stated and proved in the mathematical sense.In th~s paper, some simple heuristics combimng evaluation and mathematical reduction are described, which the authors have implemented in a program that automatlcally proves a wide varietyof theorems about recursive Lisp functions.The method the program uses to generate induction formulas is described at length The theorems proved by the program include that REVERSE is its own inverse and that a particular SORT program is correct.A list of theorems proved by the program is given KEY WORDS AND PHRASES.

It is shown how the Lisp iterative primitives PROG, SETQ, GO, and RETURN may be introduced into the Boyer-Moore method for automatically verifying Pure Lisp programs. This is done by extending some of the previously described heuristics for dealing with recursive functions. The resulting verification procedure uses structural induction to handle both recursion and iteration. The procedure does not actually distinguish between the two and they may be mixed arbitrarily. For example, since properties are stated in terms of user-defined functions, the theorem prover will prove recursively specified properties of iterative functions. Like its predecessor, the procedure does not require user-supplied inductive assertions for the iterative programs.