Books and Papers about ACL2 and Its Applications
NOTES:
 This list is generally incomplete, and many entries are
outofdate. To search for publications about some ACL2 topic we
recommend a standard web search (e.g., Google) and that you include in
your search pattern the name ACL2.
 See also the ACL2
workshops page for proceedings of ACL2 workshops, which contain numerous
papers, many of them recent, that are not found below.
 Please feel free to send us email that specifies
additions to make to the list below.
This document is divided into the following sections.
This
link will take you to a page on which you can find:
 a brief paper about ACL2 and applications;
 exercises, which provide the best way to learn ACL2;
 a paper with lots of tips on how to program and prove theorems
with ACL2; and
 additional tutorial material, including notes in Spanish and
slides by Inmaculada Medina Bulo and Francisco Palomo Lozano.
Books about ACL2 and Its Applications
 How to use ACL2:
ComputerAided Reasoning: An Approach, Matt Kaufmann,
Panagiotis Manolios, and J Strother Moore,
Kluwer Academic Publishers,
June, 2000. (ISBN 0792377443)
 What can be done with ACL2:
ComputerAided Reasoning: ACL2 Case Studies, Matt Kaufmann,
Panagiotis Manolios, and J Strother Moore (eds.),
Kluwer Academic Publishers,
June, 2000. (ISBN 0792378490)
Using the techniques described in these two books, users of the ACL2 system
have modeled and proved properties of hardware designs, microprocessors,
microcode programs, and software. In addition, many theorems in mathematics
and metamathematics have been proved with ACL2.
Details:
 ComputerAided Reasoning: An Approach: description, excerpts, errata,
solutions to exercises.
 ComputerAided Reasoning: ACL2 Case Studies: description, list of contributors, excerpts, errata,
full scripts for case studies, solutions to exercises.
 ACL2 Home Page: tours of the system, documentation, technical papers,
source code, installation guide, mailing lists.
 Ordering Information
 1999
ACL2 Wizard's Workshop: this was the meeting that produced the two books above; it
was the first in a planned series of workshops for the ACL2 community.
Book about logic in computing using ACL2
Essential
Logic for Computer Science, Rex Page and Ruben Gamboa. ISBN
9780262039185. MIT Press, 2019.
This book is an introduction to the use of predicate logic and ACL2 for
testing and verifying software and digital circuits. It has been used as a
textbook in an honors introductory course in computing, and with
supplementary materials in a course in discrete mathematics.
Book about a predecessor of ACL2
A Computational Logic, R. S. Boyer and J S. Moore.
Academic Press, New York, 1979. xiv+397.
The original Pub source for the book is here.
The translation to TeX and pdf was kindly done by Gary Klimowicz.
The above book is out of print.
The copyright has reverted to the authors.
We hereby place it in the public domain.
Book about customized reasoning tools
Scalable
Techniques for Formal Verification, Sandip Ray. ISBN
978441959973. Springer,
2010.
This book explains how to develop customized reasoning tools on
top of ACL2. The customized reasoning tools extend ACL2 by
significantly automating formal proofs on their target domains,
but without requiring any modification to the theorem prover
source code.
Design
and Verification of Microprocessor Systems for HighAssurance
Applications, David S. Hardin, ed. Springer, 2010.
Quoting from the abstract:
This book examines several leadingedge design and verification
technologies that have been successfully applied to microprocessor
systems for highassurance applications at various levels  from
arithmetic circuits to microcode to instruction sets to operating
systems to applications. We focus on recent hardware, software, and
system designs that have actually been built and deployed, and feature
systems that have been certified at high Evaluation Assurance Levels,
namely the Rockwell Collins AAMP7G microprocessor (EAL7) and the Green
Hills INTEGRITY178B separation kernel (EAL6+). The contributing
authors to this book have endeavored to bring forth truly new material
on significant, modern design and verification efforts; many of the
results described herein were obtained only within the past year.
Several chapters in this book describe ACL2 proof developments.
 ACL2 and Its Applications to Digital System
Verification, Kaufmann and Moore, pp 122
 A Mechanically Verified Commercial SRT Divider,
David M. Russinoff, pp 2364
 Use of Formal Verification at Centaur Technology,
Warren A. Hunt, Jr., Sol Swords, Jared Davis, and
Anna Slobodova, pp 6588
 Formal Verification of Partition Management for
the AAMP7G Microprocessor, Matthew M. Wilding,
David A. Greve, Raymond J. Richards, and David
S. Hardin, pp 175192
 Modeling and Security Analysis of a Commercial
RealTime Operating System Kernel, Raymond
J. Richards, pp 301322
The best introduction to ACL2 is the first of the two books above. But if
you prefer to read papers on the Web, we recommend the first two papers in Overviews.
Typical formalization problems raise many issues that are not yet adequately
addressed in ACL2 (or any other mechanized formal system). If you are trying
to formalize a problem in ACL2, you may well have to formalize some ideas for
the first time, while extending the work of others. It is often helpful to
separate the issues involved in your problem and to try to find papers below
that seem likely to touch upon some of those same issues. Then look at those
papers for ideas about how to deal with your problems. A comprehensive
set of case studies is presented in the
second of the two books above.
Several of the papers listed contain links to ACL2 scripts.
If you have a paper (preferably in postscript format) or a URL related to an
ACL2 application or extension and would like it linked into this page, please
contact moore@cs.utexas.edu
.
 About ACL2
 Enhancements
to ACL2 in Versions 6.2, 6.3, and 6.4, Matt Kaufmann and J
Strother Moore. Slides may appear later for the talk to be given
at ACL2 Workshop 2014.
 Enhancements
to ACL2 in Versions 5.0, 6.0, and 6.1, Matt Kaufmann and J
Strother Moore. Talk given
at ACL2 Workshop 2013.

ACL2 Theorems about Commercial Microprocessors, Bishop Brock, Matt
Kaufmann and J Moore, in M. Srivas and A. Camilleri (eds.) Proceedings of
Formal Methods in ComputerAided Design (FMCAD'96), SpringerVerlag,
pp. 275293, 1996. The paper sketches the system and two industrial
applications: the AMD5K86 floatingpoint division proof and the Motorola CAP
DSP model.
 An
Industrial Strength Theorem Prover for a Logic Based on Common Lisp
Matt Kaufmann and J Moore, IEEE Transactions on Software Engineering
23(4), April 1997, pp. 203213. We discuss how we scaled up the Nqthm
(``BoyerMoore'') logic to Common Lisp, preserving the use of total functions
within the logic but achieving Common Lisp execution speeds, via the
introduction of ``guards.''
 HyperCard for ACL2 Programming
by Matt Kaufmann and J Moore. This is a quick reference sheet with lots of hypertext links to the
online documentation. It also contains a gentle introduction to Lisp programming.
 A Computational Logic for Applicative Common Lisp, Matt Kaufmann and J Moore. In: A
Companion to Philosophical Logic, D. Jacquette (ed.), Blackwell Publishers,
pp. 724741, 2002.
 Design
Goals of ACL2, Matt Kaufmann and J Moore, CLI Technical Report 101,
Computational Logic, Inc., 1717 West Sixth Street, Suite 290, Austin, TX
78703, 1994. This is an early report identifying aspects of Nqthm of special
concern during the design of ACL2.
 Maintaining
the ACL2 Theorem Proving System, Matt Kaufmann and J Strother Moore. Invited
talk. Proceedings of the FLoC'06 Workshop on Empirically Successful
Computerized Reasoning, 3rd International Joint Conference on Automated
Reasoning (G. Sutcliffe, R. Schmidt, and S. Schulz, eds.), CEUR Worksho
Proceedings Vol. 192, Seattle, Washington, August 2006.
 Some Key Research Problems in Automated Theorem Proving for Hardware and
Software Verification, Matt Kaufmann and J Strother Moore.
Revista de la Real Academia de Ciencias (RACSAM), Vol. 98, No. 1, pp. 181196, 2004.
Spanish Royal Academy of Science.
 ACL2 Support for Verification Projects, Matt Kaufmann. Invited talk, Proc. 15th
Intl. Conf. on Automated Deduction, ed. C. Kirchner and H. Kirchner,
Lec. Notes Artif. Intelligence 1421, SpringerVerlag, Berlin, 1998,
pp. 220238.
 An Industrial Strength Theorem Prover for a Logic Based on Common Lisp,
Matt Kaufmann and J
Moore). IEEE Transactions on Software Engineering 23}, no. 4, April 1997,
203213.
 Design Goals for ACL2, Matt Kaufmann and J Strother Moore. In proceedings of: Third
International School and Symposium on Formal Techniques in Real Time and Fault
Tolerant Systems, Kiel, Germany (1994), pp. 92117. Published by
ChristianAlbrechtsUniversitat.

Integrating External Deduction Tools with ACL2, Matt Kaufmann, J S. Moore,
Sandip Ray, and Erik Reeber.
Journal of Applied Logic (Special Issue: Empirically Successful
Computerized Reasoning), Volume 7, Issue 1, March 2009, pp. 325.
Published online, DOI
10.1016/j.jal.2007.07.002.
Preliminary version in C. BenzmŸller,
B. Fischer, and G. Sutcliffe (eds.), Proceedings of the 6th
International Workshop on the Implementation of Logics (IWIL 2006),
Phnom Penh, Cambodia, November 2006, pages 726. Volume 212 of CEUR Workshop Proceedings.
 An Integration of HOL and ACL2, Michael J.C. Gordon, Warren
A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In Proceedings of Formal Methods in
ComputerAided Design (FMCAD'06) (A. Gupta and P. Manolios, eds.).
IEEE Computer Society Press, pp. 153160, November, 2006. Slides are available
here.
See also: An Embedding of the ACL2 Logic in HOL, Michael J.C. Gordon, Warren
A. Hunt, Jr., Matt Kaufmann, and James Reynolds. In P. Manolios and M. Wilding
(eds.), Proceedings of the 6th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),
Seattle, WA, August 2006, pages 4046. To Appear in ACM Digital Library. ©ACL2 Steering
Committee.
 Integrating CCG analysis into ACL2, Matt Kaufmann, Panagiotis Manolios, J Moore, and
Daron Vroon). Proceedings of The Eighth International Workshop on
Termination (WST 2006),
August, 2006.
 Quantification
in Tailrecursive Function Definitions, Sandip Ray. In P. Manolios and M. Wilding
(eds.), Proceedings of the 6th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),
Seattle, WA, August 2006, pages 9598. To Appear in ACM Digital Library. ©ACL2 Steering
Committee.
 Adding a Total Order to ACL2, M. Kaufmann and P. Manolios. In
Proceedings of ACL2 Workshop 2002.
 SingleThreaded Objects in ACL2, Robert
Boyer and J Moore. Singlethreaded objects in ACL2 are structures that have
the normal ``copyonwrite'' applicative semantics one expects in a
functional programming language but which are implemented by destructive
modification. The axiomatic ``story'' is consistent with the implementation
because syntactic restrictions are enforced which insure that only the
modified structure is subsequently referenced. Singlethreaded objects (or
``stobjs'') are particularly useful in modeling microprocessors, where the
state of the processor is modeled as a stobj.
 Structured Theory Development for a Mechanized
Logic, M. Kaufmann and J Moore, Journal of Automated Reasoning
26, no. 2 (2001), pp. 161203. This paper
presents a precise development of the
encapsulate
and
includebook
features of ACL2 and gives careful proofs of the
highlevel correctness properties of these ACL2 structuring mechanisms.
 A
Precise Description of the ACL2 Logic, Matt Kaufmann and J Moore, April,
1998. This paper is a working draft of a precise description of the base
logic. The draft does not describe the theorem prover or the system; it is a
dry mathematical document describing the logic from first principles. At the
moment the description omits encapsulation, multiple values, property lists,
arrays, state, and macros.
 The ACL2 User's Manual, Matt Kaufmann and J Moore.
The user's manual is a hypertext document. It is most useful in its
HTML or Texinfo forms. However, we have created a gzipped Postscript version (1.5 MB). It is roughly
1300 pages long and includes, near the end, a Table of Contents and an Index.
 Rough Diamond: An Extension of Equivalencebased Rewriting, Matt
Kaufmann and J Strother Moore. To appear, Proceedings of ITP 2014,
5th Conference on Interactive Theorem Proving. The final publication
is available at link.springer.com.
 A Futures Library and Parallelism Abstractions for a Functional
Subset of Lisp, David L. Rager, Warren A. Hunt, Jr. and Matt Kaufmann.
In Proceedings
of ELS 2011 (4th European Lisp Symposium), pp. 1316, March 31  April 1,
2011, Hamburg, Germany. This paper is relevant to ACL2(p), the
experimental extension of ACL2 supporting parallel evaluation and
proof (see :DOC PARALLELISM).
 Rewriting with Equivalence Relations in ACL2,
Bishop Brock, Matt Kaufmann, and J Strother Moore.
Journal of Automated Reasoning} 40 (2008), pp. 293306.
 Proof Search Debugging Tools in ACL2, Matt Kaufmann
and J Strother Moore. Unpublished, but presented in a talk at
Tools and Techniques for Verification
of System Infrastructure, A Festschrift in honour of Prof. Michael
J. C. Gordon FRS (Richard Boulton, Joe Hurd, and Konrad Slind,
organizers). March 2526, 2008, Royal Society, London.
 Efficient execution in an automated reasoning environment, David A. Greve, Matt
Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, Jose' Luis
RuizReina, Rob Sumners, Daron Vroon and Matthew Wilding. Journal
of Functional Programming, Volume 18, Issue 01, January 2008. Cambridge
University Press.
 Double Rewriting for Equivalential Reasoning in ACL2, Matt Kaufmann and J
Strother Moore. In P. Manolios and M. Wilding
(eds.), Proceedings of the 6th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),
Seattle, WA, August 2006, pages 103106. To Appear in ACM Digital Library. ©ACL2 Steering
Committee.
 Linear and Nonlinear Arithmetic in ACL2, Warren A. Hunt Jr.,
Robert Bellarmine Krug, and J Moore. In CHARME 2003,
D. Geist (ed.), Springer Verlag LNCS 2860, pp. 319333, 2003.
This paper describes the mechanization of linear and nonlinear
arithmetic in ACL2.
 Integrating Nonlinear Arithmetic into ACL2, Warren A. Hunt Jr.,
Robert Bellarmine Krug, and J Moore. In Proceedings of
ACL2 Workshop 2004.
This paper presents an overview of the integration of a
nonlinear arithmetic reasoning package into ACL2.
 Meta Reasoning in ACL2, Warren A. Hunt Jr, Matt Kaufmann, Robert
Bellarmine Krug, J Moore, and Eric W. Smith. In 18th
International Conference on Theorem Proving in Higher Order
Logics: TPHOLs 2005, J. Hurd and T. Melham (eds.), Springer
Lecture Notes in Computer Science, 3603, pp. 163178, 2005.
This paper describes the variety of metareasoning facilities
in ACL2.

Attaching Efficient Executability to Partial Functions in ACL2,
Sandip Ray.
In M. Kaufmann and J S. Moore (eds.), 5th
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2004), Austin, TX, November 2004.
 A Tool for Simplifying Files of ACL2 Definitions, Matt Kaufmann. In
Proceedings
of ACL2 Workshop 2003. If you obtain the workshops books, see
books/workshops/2003/kaufmann/
.
 ACL2 Interaction via Emacs, Bishop Brock, 1998. This is a collection
of Emacs programs to speed up interaction between ACL2 and Emacs. If you
typically interact with ACL2 via an Emacs buffer, you may be surprised to
know that up to half of the time you spend waiting for an ACL2 command to
complete is due to Emacs display overhead. This package includes freely
distributable source code for two effective approaches to reducing this
overhead. The first approach is very general and provides pretty good
results. The other approach is a bit of a hack, but practically eliminates
display overhead for long ACL2 runs. To try these out, download the
following file. You should name the file
acl2emacs.tar.gz
.
After downloading it, decompress and untar it with
% tar xvzf acl2emacs.tar.gz
and read the enclosed note in report.ps
. Here is the file to
download, but don't click on it as you would a normal link or you may get a
browser screen of gibberish. Click on it to download (e.g., in Netscape,
Shift+Button 1 (hold shift and click the left mouse button) or Button 3 and
then select ``Save link as...''). acl2emacs.tar.gz
 Infix Printing, Mike Smith, 1998.
An infix syntax for ACL2 has been implemented by Mike Smith. Two
capabilities are supported.
 IACL2 is an infix version of the ACL2
theorem proving system that performs I/O in infix
format. It is intended to make initial
experiments with ACL2 somewhat simpler for those unfamiliar with or
opposed to Lisp prefix syntax. (It is not an interface for experts, as
some of the more advanced aspects of ACL2 are not supported by the
infix parser.) Some examples of the syntax:
Function idiv (m : integer, n : integer  n ~~= 0)
{ ifix ( m/n ) };
/* Idiv takes two integer arguments, the second of which cannot = zero */
Theorem distributivityofminusoverplus
{(x + y) = x + y};
Theorem carnth0 { consp(x) > x.car = x[0] };
 We provide formatting support to help the user publish ACL2 event
files. The syntax produced is either standard ACL2 or ``conventional''
infix mathematical notation with formatted comments and
docstrings. For example, in LaTeX mode comments are formatted as
running text, events are indexed and substitutions are made of LaTeX
mathematical symbols for various functions. In HTML mode, cross
references are created from function usage to definition. Other ouput
modes include Scribe and ASCII text. The formatting conventions are
user extensible.
For more information, see the
README overview.
 Finite set theory based on fully ordered lists, by Jared Davis,
describes the set theory implementation in
books/finitesettheory/osets/
. In this
library, set equality is just ACL2's "equal" and the typical set
operations (union, intersection, difference, cardinality) are
lineartime and efficiently implemented. A fairly complete set of set
operations and rewrite rules are provided, and "pick a point" proofs
can be used to show subset relations. Macros allow the quick
introduction of functions to quantify predicates over sets (e.g.,
"alllessthan"), and map functions over sets (e.g.,
"consontoeach"). More information and
slides are also available at the above page.
 Finite Set Theory in ACL2, by J
Strother Moore, describes some of the features available in the
distributed book
books/finitesettheory/settheory.lisp
. The book provides
hereditarily finite sets built from ACL2 objects. Sets are represented by
lists. Sets may contain sets as elements. The usual primitives  including
those for dealing with functions as sets of ordered pairs  are defined and
lemmas are proved providing many algebraic properties of finite set theory.
Some common proof strategies are codified and macros are provided for
defining functions that construct certain sets from others. This book is
just a start at what could easily turn into a major effort to support finite
set theory more completely.
 Efficient
Rewriting of Data Structures in ACL2, M. Kaufmann and R. Sumners.
In Proceedings of
ACL2 Workshop 2002 This paper describes the socalled "records books",
distributed in
books/misc/records.lisp
and books/misc/records0.lisp
.
 An Exercise in Graph Theory, J Moore, Chapter 5 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/graph/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
The article formalizes and proves the correctness of several
simple algorithms for determining whether a path exists between two nodes of
a finite directed graph. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.

Defthms About Zip and Tie: Reasoning About Powerlists in ACL2, Ruben
Gamboa, University of Texas Computer Sciences Technical Report No. TR9702,
February, 1998. This work is based on Jay Misra's ``powerlist'' device, a
data structure wellsuited to recursive, dataparallel algorithms. A
generalization of powerlists is formalized in ACL2 by Gamboa and used to
prove a variety of algorithm correct, including several sorting algorithms
(including bitonic and Batcher), a greycode sequence generator, and a
carrylookahead adder. ACL2 event lists are linked to the URL above.
 Mechanically
Verifying the Correctness of the Fast Fourier Transform in ACL2, Ruben
Gamboa, in Third International Workshop on Formal Methods for Parallel
Programming: Theory and Applications (FMPPTA), 1998. This paper is based on
Jay Misra's work on ``powerlists'' (above) and formalizes Misra's
stunningly simple proof of the correctness of an FFT algorithm implemented
with powerlists. The URL above links to an ACL2 event script as well.
 Defstructure
for ACL2, Bishop Brock, December, 1997. This paper serves as
documentation for the ACL2
defstructure
book, which provides a
``record facility'' similar to Common Lisp's defstruct
and
Nqthm's addshell
.
See also the previously mentioned book, "Design
and Verification of Microprocessor Systems for HighAssurance
Applications", for a variety of papers by various authors on
processing modeling in ACL2 (and other systems).

Modeling
and Verification of Industrial Flash Memories. S. Ray, J. Bhadra,
T. Portlock, and R. Syzdek. In P. Chatterjee and K. Gadepally,
editors, Proceedings of the 11th
International Symposium on Quality Electronic Design (ISQED 2010),
San Jose, CA, March 2010, pages 705712. IEEE.

Optimizing
Equivalence Checking for Behavioral Synthesis. K. Hao, F. Xie,
S. Ray, and J. Yang. In Design, Automation & Test in
Europe (DATE 2010), Dresden, Germany, March 2010. IEEE.

Connecting
Presilicon and Postsilicon Verification.
S. Ray and W. A. Hunt, Jr.
In A. Biere and C.
Pixley, editors, Proceedings of the 9th International Conference on
Formal Methods in Computeraided Design (FMCAD 2009), Austin, TX,
November 2009, pages 160163. IEEE Computer
Society.

Formal
Verification for HighAssurance Behavioral Synthesis.
S. Ray, K. Hao, Y. Chen, F. Xie, and J. Yang.
In Z. Liu and A. P. Ravn, editors, Proceedings
of the 7th International
Symposium on Automated Technology for Verification and Analysis (ATVA
2009), Macao SAR, China, October 2009, volume 5799 of LNCS, pages
337351. Springer.

Abstracting
and Verifying Flash Memories, Sandip Ray and Jayanta Bhadra. In K. Campbell, editor,
Proceedings of the 9th NonVolatile
Memory Technology Symposium (NVMTS 2008), Pacific Grove, CA,
November 2008, pages 100104. IEEE.

A
Mechanized Refinement Framework for Analysis of Custom Memories,
Sandip Ray and Jayanta Bhadra.
In J. Baumgartner and M. Sheeran, editors,
Proceedings of the 7th
International Conference on Formal Methods in Computeraided Design
(FMCAD 2007), Austin, TX, November 2007, pages 239242. IEEE Computer
Society.

Mechanized
Certification of Secure Hardware Designs, Sandip Ray and Warren
A. Hunt, Jr. In J. Bhadra, L. Wang, and M. S. Abadir,
editors, Proceedings of the 8th
International Workshop on Microprocessor Test and Verification, Common
Challenges and Solutions (MTV 2007), Austin, TX, December 2007.
IEEE Computer
Society.
 Formal Verification of FloatingPoint RTL at AMD using the ACL2 Theorem Prover,
David Russinoff, Matt Kaufmann, Eric Smith, Robert Sumners. 17th IMACS World
Congress: Scientific Computation, Applied Mathematics and Simulation. July,
2005.

Deductive Verification of Pipelined Machines Using Firstorder
Quantification, Sandip Ray and Warren A. Hunt Jr.
In R. Alur and D. A. Peled, editors, Proceedings of the
16th International Conference on Computeraided Verification (CAV 2004),
Boston, MA, July 2004, volume 3117 of LNCS, pages 3143. ©SpringerVerlag.
 Formal Verification
of Microprocessors at AMD, Arthur Flatau, Matt Kaufmann, David F. Reed, David Russinoff,
Eric Smith, and Rob Sumners. Proceedings of Designing Correct Circuits 2002.
 HighSpeed, Analyzable Simulators, David Greve, Matthew Wilding, and
David Hardin, Chapter 8 of ComputerAided
Reasoning: ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer,
2000.
(ACL2 scripts are available from
directory
1999/simulator/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
Highspeed simulation models are routinely developed during the
design of complex hardware systems in order to predict performance, detect
design flaws, and allow hardware/software codesign. Writing such an
executable model in ACL2 brings the additional benefit of formal analysis;
however, much care is required to construct an ACL2 model that is both fast
and analyzable. In this article, techniques are described for the
construction of highspeed formally analyzable simulators in ACL2. Their
utility is demonstrated on a simple processor model. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
 Verification of a Simple Pipelined Machine Model, Jun Sawada, Chapter 9
of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/pipeline/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
An ACL2 model of a threestage pipelined machine is defined,
along with a model of the corresponding sequential machine. Then a proof of
the equivalence between the two machines is presented. More importantly, the
method of decomposing the proof applies to much more complicated pipelined
architectures. The ACL2 scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.
 Verification of Pipeline Circuits, Matt Kaufmann and David M. Russinoff, in
Proceedings of
ACL2 Workshop 2000.
 The DE Language, Warren Hunt, Jr., Chapter 10 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/dehdl/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
The DE language is an occurrenceoriented description language
that permits the hierarchical definition of finitestate machines in the
style of a hardware description language. The syntax and semantics of the
language are formalized and the formalization is used to prove the
correctness of a simple hardware circuit. Such formal HDLs have been used to
prove properties of much more complicated designs. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
 Using Macros to Mimic VHDL, Dominique Borrione, Philippe Georgelin, and
Vanderlei Rodrigues, Chapter 11 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/vhdl/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
The purpose of this project was to formalize a small
synthesizable behavioral subset of VHDL, preserving as much as possible the
syntactic flavor of VHDL and facilitating verification by symbolic simulation
and theorem proving. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.
 Efficent
Simulation of Formal Processor Models, Dave Hardin, Matt
Wilding, and Dave Greve, Rockwell Collins, Inc., Advanced Technology Center,
Cedar Rapids, IA, May, 1998. This paper describes some ``hacks'' by which
ACL2 array processing can be sped up to C speeds. A simple processor model,
comparable to the traditional ``small machine'' mentioned above, is used as
the benchmark. Native ACL2 achieves simulation speeds of about 19,000
``small machine'' instructions per second when executing this model. After
modifying ACL2 as described, the model is executed at slightly over 2 million
instructions per second, comparable to a C model of the processor.
Technically, the techniques used in this paper render ACL2 unsound because
they assume (without the necessary syntactic checking) that ACL2 arrays are
used in a singlethreaded way. However, the experiments done in this paper
and the techniques used are extremely illuminating. They also indicate
modifications that could be made to ACL2 to provide the efficiency needed in
industrialscale modeling, while preserving soundness. The paper is highly
recommended.
 Transforming
the Theorem Prover into a Digital Design Tool: From Concept Car to OffRoad
Vehicle, Dave Hardin, Matt Wilding and Dave Greve, in A. J. Hu and
M. Y. Vardi (eds.) Computer Aided Verification: 10th International
Conference, CAV '98, SpringerVerlag LNCS 1427, 1998. The paper
suggests ways to integrate theorem proving into the microprocessor design
cycle. The paper was presented at CAV '98. During the talk, the authors
demonstrated an ACL2 model of the ALU of the JEM1 (a silicon Java Virtual
Machine) microprocessor, its transparent use to compute ALU results for a
Cbased simulation tool for the processor and ACL2 proofs about the ALU.
This demonstration is not discussed in the paper but is indicative of the
ideas in the paper.
 Symbolic Simulation: An ACL2 Approach, J Moore,
in G. Gopalakrishnan and P. Windley (eds.)
Proceedings of the Second International Conference on Formal Methods
in ComputerAided Design (FMCAD'98), SpringerVerlag LNCS 1522,
pp. 334350, November, 1998.
(
ACL2 Script) This paper advocates the idea of symbolic simulation of
processor models, as a step from the familiar (namely, traditional simulation
of C models of designs) to the unfamiliar (namely, proofs about formal
models). The papers demonstrates how ACL2 can provide a symbolic simulation
capability for the ``small machine'' model. Some interesting performance
measures are also given.

Mechanized
Information Flow Analysis through Inductive Assertions, Warren A. Hunt, Jr., Robert Bellarmine Krug, Sandip Ray, and William
D. Young. In A. Cimatti and R. B. Jones, editors,
Proceedings of the 8th
International Conference on Formal Methods in Computeraided Design
(FMCAD 2008), Portland, OR, November 2008, pages 227230. IEEE Computer
Society.

Evaluating SFI for a CISC Architecture by Stephen McCamant and Greg
Morrisett. In 15th USENIX Security Symposium, (Vancouver, BC, Canada),
August 24, 2006, pp. 209224. See also the project page.

Mechanized Operational
Semantics by J Moore (lectures given at Marktoberdorf Summer
School 2008). These lectures explain how to formalize an
``operational'' or ``statetransition'' semantics of a von Neumann
programming language in a functional programming language.
These lectures illustrate the techniques by formalizing a simple
programming language called ``M1,'' for ``Machine (or Model) 1.'' It
is loosely based on the Java Virtual Machine but has been simplified
for pedagogical purposes. They demonstrate the executability of M1
models. Several styles of code proofs are developed, including direct
(symbolic simulation) proofs based on BoyerMoore ``clock functions''
and FloydHoare inductive assertion proofs. Proofs are constructed
only for the simplest of programs, namely an iterative factorial
example. But to illustrate a more realistic use of the model, the
correctness proof for an M1 implementation of the BoyerMoore fast
string searching algorithm is discussed.

A
Mechanical Analysis of Program Verification Strategies, Sandip Ray, Warren
A. Hunt, Jr. John Matthews, and J Strother Moore. Journal of
Automated Reasoning. volume 40(4), May 2008, pages 245269. Springer.

Verification Condition Generation via Theorem Proving, John Matthews, J
S. Moore, Sandip Ray, and Daron Vroon. In M. Hermann and
A. Voronkov, editors, Proceedings of the 13th International Conference on Logic
for Programming, Artificial Intelligence, and Reasoning (LPAR 2006), Phnom Penh,
Cambodia, November 2006, volume 4246 of LNCS, pages 362376. ©SpringerVerlag
 A Verifying Core for a Cryptographic Language Compiler, Lee Pike,
Mark Shields, and John Matthews. In P. Manolios and M. Wilding
(eds.), Proceedings of the 6th International
Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2006),
Seattle, WA, August 2006, pages 9598. To Appear in ACM Digital Library. ©ACL2 Steering
Committee. See also the supporting
materials.

Proof Styles in Operational Semantics, Sandip Ray and J S. Moore.
In A. J. Hu and A. K. Martin,
editors, Proceedings of the 5th International Conference on Formal Methods in
Computeraided Design (FMCAD 2004), Austin, TX, November 2004, volume 3312
of LNCS, pages 6781. ©SpringerVerlag.
 Design Verification of a SafetyCritical Embedded Verifier, Piergiorgio
Bertoli and Paolo Traverso, Chapter 14 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/embedded/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
This article shows the use of ACL2 for the design verification of
a piece of safetycritical software, the Embedded Verifier. The Embedded
Verifier checks online that each execution of a safetycritical translator is
correct. The translator is a component of a software system used by Union
Switch and Signal to build trainborne control systems. The ACL2 scripts
referenced here provide the full details of the results described in the
article along with solutions to all the exercises in the article.
 Compiler Verification Revisited, Wolfgang Goerigk, Chapter 15 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/compiler/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
This study illustrates a fact observed by Ken Thompson in his
Turing Award Lecture: the machine code of a correct compiler can be altered
to contain a Trojan Horse so that the compiler passes almost every test,
including the socalled ``bootstrap test'' in which it compiles its own
source code with identical results, and still be capable of generating
``bad'' code. The compiler, the object code machine, and the experiments are
formalized in ACL2. The ACL2 scripts referenced here provide the full
details of the results described in the article along with solutions to all
the exercises in the article.
 Proving Theorems about Javalike Byte Code, J
Moore, in E.R. Olderog and B. Steffen (eds.) Correct System Design 
Recent Insights and Advances, LNCS: StateoftheArtSurvey, Volume 1710,
pp. 139162, 1999). This paper describes a formalization of an abstract
machine very similar to the Java Virtual Machine but far simpler. Techniques
are developed for specifying the properties of classes and methods for this
machine. The paper illustrates two such proofs, that of a static method
implementing the factorial function and of an instance method that
destructively manipulates objects in a way that takes advantage of
inheritance. An ACL2 Script is also available.
 Mechanized
Formal Reasoning about Programs and Computing Machines, Bob Boyer and J
Moore, in R. Veroff (ed.), Automated Reasoning and Its Applications:
Essays in Honor of Larry Wos, MIT Press, 1996. This paper explains a
formalization style that has been extremely successful in enabling
mechanized reasoning about programs and machines, illustrated in ACL2. This
paper presents the socalled ``small machine'' model, an extremely simple
processor whose state consists of the program counter, a RAM, an executeonly
program space, a control stack and a flag. The paper explains how to prove
theorems about such models. Accompanying the paper is an
ACL2 Script: After fetching this script, use
includebook
to
load it into your ACL2 and then do (inpackage "SMALLMACHINE")
.
 A Formal Theory of RegisterTransfer Logic
and FloatingPoint Arithmetic, David Russinoff. This is a user's manual for an ACL2 library
of floatingpoint arithmetic as well as an exposition of the underlying theory.

A Case Study in Formal Verification of RegisterTransfer Logic with ACL2:
The Floating Point Adder of the AMD Athlon Processor, David Russinoff.
Invited paper in Warren A. Hunt Jr. and
Steven D. Johnson (eds.), Proceedings of the Third International Conference on Formal Methods
in ComputerAided Design (FMCAD 2000), SpringerVerlag LNCS 1954, 2000.
This is a proof of IEEEcompliance, as an application of a mechanical proof system for RTL designs based
on ACL2.
 RTL Verification: A FloatingPoint Multiplier, David M. Russinoff and
Arthur Flatau, Chapter 13 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/multiplier/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
This article describes a mechanical proof system for designs
represented in the RTL language of Advanced Micro Devices. The system
consists of a translator to ACL2 and a methodology for verifying properties
of the resulting programs using the ACL2 prover. The correctness of a simple
floatingpoint multiplier is proved. The ACL2 scripts referenced here
provide the full details of the results described in the article along with
solutions to all the exercises in the article.
 A Mechanically Checked Proof of the
Correctness of the Kernel of the AMD5K86 FloatingPoint Division
Algorithm, J Moore, Tom Lynch, and Matt Kaufmann, IEEE Transactions on
Computers, 47(9), pp. 913926, Sep., 1998. This is the original (
March, 1996) version of our paper describing the mathematical details of the
proof that the FDIV microcode on the AMD K5 correctly implements IEEE
floating point division. The paper underwent extensive revision during the
reviewing process.
 A
Mechanically Checked Proof of IEEE Compliance of a RegisterTransferLevel
Specification of the AMD K7 Floating Point Multiplication, Division and
Square Root Instructions, David Russinoff, Advanced Micro Devices, Inc.,
January, 1998. This paper is a tour de force in mechanical
verification. The paper describes a mechanically verified proof of
correctness of the floatingpoint multiplication, division, and square root
instructions of The AMD K7 microprocessor. The instructions, which are based
on Goldschmidt's Algorithm, are implemented in hardware and represented by
registertransfer level specifications, the primitives of which are logical
operations on bit vectors. On the other hand, the statements of correctness,
derived from IEEE Standard 754, are arithmetic in nature and considerably
more abstract. Therefore, the paper develops a theory of bit vectors and
their role in floatingpoint representations and rounding, extending previous
work (below) in connection with the K5 FPU. The paper then presents the
hardware model and a rigorous and detailed proof of its correctness. All of
the definitions, lemmas, and theorems have been formally encoded in the ACL2
logic, and every step in the proof has been mechanically checked with the
ACL2 prover.
 A Mechanically
Checked Proof of IEEE Compliance of the AMD K5 FloatingPoint Square Root
Microcode, David Russinoff, Formal Methods in System Design
Special Issue on Arithmetic Circuits, 1997. The paper presents a rigorous
mathematical proof of the correctness of the FSQRT instruction of the AMD K5
microprocessor. The instruction is represented as a program in a formal
language that was designed for this purpose, based on the K5 microcode and
the architecture of its FPU. The paper proves a statement of its correctness
that corresponds directly with the IEEE standard. It also derives an
equivalent formulation, expressed in terms of rational arithmetic, which has
been encoded as a formula in the ACL2 logic and mechanically verified with
the ACL2 prover. Finally, the paper describes a microcode modification that
was implemented as a result of this analysis in order to ensure the
correctness of the instruction.
 NonStandard
Analysis in ACL2, Ruben A. Gamboa and Matt Kaufmann, Journal of Automated
Reasoning 27(4), 323351, 2001.
This paper describes
ACL2(r), a version of ACL2 with support for the real and complex numbers. The
modifications are based on nonstandard analysis, which interacts better with
the discrete flavor of ACL2 than does traditional analysis. See below for a little more about ACL2(r).
 Modular Proof: The Fundamental Theorem of Calculus, Matt Kaufmann,
Chapter 6 of ComputerAided Reasoning:
ACL2 Case Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/calculus/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
The article presents a modular topdown proof methodology and
uses it to formalize and prove the Fundamental Theorem of Calculus. The
modular strategy works for both ACL2 and ``ACL2(r)'' (see above); the
Fundamental Theorem is proved with ACL2(r). The ACL2 scripts referenced here
provide the full details of the results described in the article along with
solutions to all the exercises in the article.
 Continuity and Differentiability, Ruben Gamboa, Chapter 18 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/analysis/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
This article shows how an extended version of ACL2 (named
``ACL2(r)'' and described below) can be used to reason about the real and
complex numbers, using nonstandard analysis. It describes some
modifications to ACL2 that introduce the irrational real and complex numbers
into ACL2's number system. It then shows how the modified ACL2 can prove
classic theorems of analysis, such as the intermediatevalue and meanvalue
theorems. The ACL2(r) scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.
 ACL2 supports the rational numbers but not the reals. Starting with
Version 2.5, however, a variant of ACL2 called ``ACL2(r)'' supports the real
numbers by way of nonstandard analysis. ACL2(r) was produced by Ruben
Gamboa from ACL2. ACL2(r) can be built from the ACL2 sources (Versions 2.5
and higher). See the makefile for instructions for building ACL2(r). For
further acknowledgements and some technical details see the documentation
topic
REAL
in the online documentation for ACL2. ACL2 authors
Kaufmann and Moore consider ACL2(r) Version 2.5 to be in ``beta release.''
They have tried to ensure that when ACL2 is built from the integrated source
files, the result is a sound ACL2. They are confident that ACL2(r) will
eventually be sound and behave much as it does in the Version 2.5 release,
but have not yet checked every detail of the integration. For the
foundations of ACL2(r), see Gamboa's Ph.D. dissertation Mechanically Verifying
RealValued Algorithms in ACL2 (UT, May, 1999). The dissertation
includes ACL2(r)checked proofs of many fundamental properties of the real
numbers, including such results as the continuity of e^x
,
Euler's identity, the basic identities of trigonometry, the intermediate
value theorem, and others.
 Square
Roots in ACL2: A Study in Sonata Form, Ruben Gamboa, UTCS Tech Report
TR9634, November, 1996. This paper describes a proof in ACL2 that
(*
x x)
is never 2. This was the beginning of Gamboa's journey into
the ACL2 mechanization of nonstandard analysis.
 A Mechanically Checked Proof of a
Multiprocessor Result via a Uniprocessor View, J Moore, February, 1998.
This paper presents an ACL2 proof that an nprocessor concurrent system
implements a nonblocking counter. This paper illustrates one method for
dealing with concurrency and nondeterminism in ACL2, by formalizing a
compositional semantics for a sharedmemory concurrent system. ( ACL2 script).
 An ACL2 Proof of Write Invalidate Cache
Coherence, J Moore, in A. J. Hu and M. Y. Vardi (eds.) Computer Aided
Verification: 10th International Conference, CAV '98, SpringerVerlag
LNCS 1427, pp. 2938, 1998. This paper presents a pedagogical example of
the use of ACL2. An extremely simple cache coherence property is formalized
and proved. The intended contribution of the paper is not in the realm of
cache coherence  the problem dealt with here is far too simple for that 
but in demonstrating the ACL2 in a simple modeling project and in one
approach to concurrency. (ACL2
Scripts)
 Interactive
Consistency in ACL2, Bill Young, Computational Logic, Inc., March,
1997. This paper presents an ACL2 translation of Rushby's PVS improvement
to Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport
Oral Messages (``Byzantine Generals'') problem.
 The
Right Tools for the Job: Correctness of Cone of Influence Reduction
Proved Using ACL2 and
HOL4,
M. J. C. Gordon,
M. Kaufmann,
and S. Ray.
Journal
of Automated Reasoning, volume 47(1), June 2011, pages
116. Springer.

Combining
Theorem Proving with Model Checking through Predicate Abstraction,
Sandip Ray and Rob Sumners.
IEEE Design & Test of
Computers, volume 24(2), MarchApril 2007 (Special Issue on
Advances in Functional Validation through Hybrid Techniques), pages
132139.

Reducing Invariant Proofs to Finite Search via Rewriting,
Rob Sumners and Sandip Ray.
In M. Kaufmann
and J S. Moore, editors, 5th
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2004), Austin, TX, November 2004.

Certifying Compositional Model Checking Algorithms in ACL2,
Sandip Ray, John Matthews, and Mark Tuttle.
In 4th
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2003), Boulder, CO, July 2003.
 MuCalculus ModelChecking, Panagiotis Manolios, Chapter 7 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/mucalculus/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
The article presents a formal development of the syntax and
semantics for the Mucalculus, a modelchecker for it in ACL2, and a
discussion of the translation of other temporal logics into the Mucalculus.
The model checker is proved correct. The ACL2 scripts referenced here
provide the full details of the results described in the article along with
solutions to all the exercises in the article.
 Symbolic Trajectory Evaluation, Damir A. Jamsek, Chapter 12 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/ste/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
Symbolic Trajectory Evaluation (STE) is a form of model checking
fundamentally based on symbolic simulation. This article presents a formal
treatment of STE, including ACL2 proofs of results presented in the Seger and
Joyce paper ``A Mathematically Precise TwoLevel Formal Hardware Verification
Methodology.'' The ACL2 scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.

Formal Correctness of a Quadratic Unification Algorithm,
J.L. RuizReina, F.J. MartínMateos, J.A. Alonso and M.J. Hidalgo.
Journal of Automated Reasoning (37):12, pp. 6792, 2006.
The paper presents the formal verification of a syntactic unification
algorithm of quadratic time complexity, using a dag representation for
terms. The use of stobjs and defexec/mbe makes the algorithm efficiently
executable.

Proof Pearl: A Formal Proof of Higman's Lemma in ACL2,
F.J. MartínMateos, J.L. RuizReina, J.A. Alonso and M.J. Hidalgo.
Journal of Automated Reasoning (47):3, pp. 229250, 2011.
Highman's Lemma is a property about well quasiorderings on strings. In
this paper a formal proof of this result is presented, using a termination
argument based on wellfounded multiset extensions.

A Formal Proof of Dickson's Lemma in ACL2,
F.J. MartínMateos, J.A. Alonso, M.J. Hidalgo and J.L. RuizReina.
LPAR 2003  LNAI 2850, pp. 4958, 2003.
Dickson's Lemma is the main result needed for proving termination of
Buchberger's algorithm for computing Gröbner basis of ideals of
polynomials. In this paper a formal proof of this result is presented,
using a termination argument based on wellfounded multiset extensions.

Formal verification of a generic framework to synthesize SATprovers,
F.J. MartínMateos, J.A. Alonso, M.J. Hidalgo and J.L. RuizReina.
Journal of Automated Reasoning (32):4, pp. 287313, 2004.
A generic framework for SAT checkers is defined and verified. Several
verified and executable SAT solvers can be obtained instantiating this
generic framefork.

Termination in ACL2 Using Multiset Relations,
J.L. RuizReina, J.A. Alonso, M.J. Hidalgo and F.J. MartínMateos.
Thirty Five Years of Automating Mathematics, pp. 217245. 2003.
A proof in ACL2 of the wellfoundedness of multiset extensions of
wellfounded relations and a tool for generating automatically such
multiset relations.

A certified polynomialbased decision procedure for propositional logic ,
I. Medina Bulo, F. Palomo Lozano and J. A. Alonso Jiménez, 4th
International Conference on Theorem Proving in Higher Order Logics , LNCS
2152:297312. Edinburgh (Escocia), 2001. In this paper we present the
formalization of a decision procedure for Propositional Logic based on
polynomial normalization. This formalization is suitable for its automatic
verification in an applicative logic like ACL2. This application of
polynomials has been developed by reusing a previous work on polynomial
rings, showing that a proper formalization leads to a high level of
reusability. Two checkers are defined: the first for contradiction formulas
and the second for tautology formulas. The main theorems state that both
checkers are sound and complete. Moreover, functions for generating models
and counterexamples of formulas are provided. This facility plays also an
important role in the main proofs. Finally, it is shown that this allows for
a highly automated proof development.

Formal Proofs About Rewriting Using ACL2,
J.L. RuizReina, J.A. Alonso, M.J. Hidalgo and F.J. MartínMateos.
Annals of Mathematics and Artificial Intelligence 36(3),
pp. 239262, 2002.
This paper presents a formalization of term rewriting systems. That is,
ACL2 is used as the metatheory to formalize results in equational
reasoning and rewrite systems. Notions such as confluence, local
confluence, and normal forms are formalized. The main theorems proved are
Newman's Lemma and KnuthBendix criticalpair theorem.
 Ivy: A Preprocessor and Proof Checker for FirstOrder Logic, William
McCune and Olga Shumsky, Chapter 16 of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/ivy/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
In this case study, a proof checker for firstorder logic is
proved sound for finite interpretations. In addition, the study shows how
nonACL2 programs can be combined with ACL2 functions in such a way that
useful properties can be proved about the composite programs. Nothing is
proved about the nonACL2 programs. Instead, the results of the nonACL2
programs are checked at run time by ACL2 functions, and properties of these
checker functions are proved. The ACL2 scripts referenced here provide the
full details of the results described in the article along with solutions to
all the exercises in the article.
 Verifying the
bridge between simplicial topology and algebra: the EilenbergZilber
algorithm, L. Lambán, J. Rubio, F. J. MartínMateos and
J. L. RuizReina. Logic Journal of the IGPL 22(1),
pp. 3965, 2014. The EilenbergZilber algorithm is one of the central
components of the computer algebra system called Kenzo, devoted
to computing in Algebraic Topology. In this article we report on a
complete formal proof of the underlying
EilenbergZilber theorem, using the ACL2 theorem prover. As our
formalization is executable, we are able to compare the results of the
certified programme with those of Kenzo on
some universal examples. Since the results coincide, the
reliability of Kenzo is reinforced. This is a new step in our
longterm project towards certified programming for Algebraic
Topology.
 [Note: This entry extends an earlier version, included just below.]
Formalization of a normalization theorem in simplicial
topology, L. Lambán, F. J. MartínMateos,
J. Rubio and J. L. RuizReina. Annals of Mathematics and
Artificial Intelligence 64(1), pp. 137, 2012. In this paper
we present a complete formalization of the Normalization Theorem,
a result in Algebraic Simplicial Topology stating that there
exists a homotopy equivalence between the chain complex of a
simplicial set, and a smaller chain complex for the same
simplicial set, called the normalized chain complex. Even if the
Normalization Theorem is usually stated as a higherorder result
(with a Category Theory flavor) we manage to give a firstorder
proof of it. To this aim it is instrumental the introduction of an
algebraic data structure called simplicial polynomial. As a
demonstration of the validity of our techniques we developed a
formal proof in the ACL2 theorem prover.
 [Note: See entry just above for an extended version.]
Applying ACL2 to the Formalization of Algebraic Topology: Simplicial
Polynomials, L. Lambán, F. J. MartínMateos, J. Rubio
and J. L. RuizReina. ITP 2011  LNCS 6898, pp. 200215, 2011.
In this paper we present a complete formalization of the Normalization
Theorem, a result in Algebraic Simplicial Topology stating that there
exists a homotopy equivalence between the chain complex of a simplicial
set, and a smaller chain complex for the same simplicial set, called the
normalized chain complex.

ACL2 verification of simplicial degeneracy programs in the Kenzo
system,
F.J. MartínMateos, J. Rubio and J.L. RuizReina.
Calculemus 2009  LNAI 5625, pp. 106121, 2009.
In this paper, we give a complete automated proof of the correctness of
the encoding of degeneracy lists (a topological object) used in Kenzo,
a Computer Algebra System devoted to Algebraic Topology.
 A verified
Common Lisp implementation of Buchberger's algorithm in ACL2.
I. Medina Bulo, F. Palomo Lozano, and J. L. Ruiz Reina. Journal of
Symbolic Computation 451:96123. 2010. In this article, we
present the formal verification of a Common Lisp implementation of
Buchberger's algorithm for computing Gröbner bases of polynomial
ideals. This work is carried out in ACL2, a system which provides an
integrated environment where programming (in a pure functional subset
of Common Lisp) and formal verification of programs, with the
assistance of a theorem prover, are possible. Our implementation is
written in a real programming language and it is directly executable
within the ACL2 system or any compliant Common Lisp system. We provide
here snippets of real verified code, discuss the formalization details
in depth, and present quantitative data about the proof effort.

Formal Verification of Molecular Computational Models in ACL2:
A Case Study,
F.J. MartínMateos, J.A. Alonso, M.J. Hidalgo and J.L. RuizReina.
CAEPIA 2003  LNCS 3040, pp. 344353, 2004.
A formalization in ACL2 of Lipton's experiment that uses DNA computation
for solving SAT.

Verified Computer Algebra in ACL2 (Gröbner Bases Computation), I.
Medina Bulo, F. Palomo Lozano, J. A. Alonso Jiménez and J. L. Ruiz
Reina, Artificial Intelligence and Symbolic Mathematical Computation
(AISC 2004) , LNAI 3249:171184. Linz (Austria), 2004. In this paper, we
present the formal verification of a Common LISP implementation of
Buchberger's algorithm for computing Gröbner bases of polynomial ideals.
This work is carried out in the ACL2 system and shows how verified Computer
Algebra can be achieved in an executable logic.

Verification of an Inplace Quicksort in ACL2, Sandip Ray and Rob Sumners.
In D. Borrione, M. Kaufmann,
and J S. Moore, editors, Proceedings of the 3rd
International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2
2002), Grenoble, France, April 2002, pages 204212.
 A Mechanical Proof of the
Chinese Remainder Theorem, David Russinoff, in Proceedings of
ACL2 Workshop 2000.
 Knuth's Generalization of McCarthy's 91 Function, John Cowles, Chapter 17
of ComputerAided Reasoning: ACL2 Case
Studies (Kaufmann, Manolios, Moore, eds.) Kluwer, 2000.
(ACL2 scripts are available from
directory
1999/knuth91/
if you
fetch the workshops books from the downloads page of the
acl2books project website.)
This article deals with a challenge by Donald Knuth for a ``proof
by computer'' of a theorem about his generalization of John McCarthy's famous
``91 function.'' The generalization involves real numbers, and the case
study uses ACL2 to meet Knuth's challenge by mechanically verifying results
not only about the field of all real numbers, but also about every subfield
of that field. The ACL2 scripts referenced here provide the full details of
the results described in the article along with solutions to all the
exercises in the article.

Verification of Year 2000 Conversion Rules, Matt Kaufmann, March 1999
(revised from June 1999). This page links to event files in support
of the paper "Verification of Year 2000 Conversion Rules Using the
ACL2 Theorem Prover," to appear in Software Tools for
Technology Transfer. This formal verification of COBOL
transformation rules was done in support of Y2K remediation performed
at EDS CIO Services using an inhouse proprietary tool, Cogen 2000.
 A Mechanically Checked Proof of a Comparator Sort Algorithm,
J Moore and B. Brock,
in, M. Broy, J. Gruenbauer, D. Harel, and
C. A. R. Hoare (eds.)
Engineering Theories of Software Intensive Systems,
Springer NATO Science Series II, 195, pp. 141175, 2005.
This paper describes a mechanically checked correctness proof for the
comparator sort algorithm underlying a microcode program in a commercially
designed digital signal processing chip. The abstract algorithm uses an
unlimited number of systolic comparator modules to sort a stream of data. In
addition to proving that the algorithm produces an ordered permutation of its
input, two theorems are proved that are important to verifying the microcode
implementation. These theorems describe how positive and negative
``infinities'' can be streamed into the array of comparators to achieve
certain effects. Interesting generalizations are necessary in order to prove
these theorems inductively.
(ACL2 Script)
 The
Specification of a Simple Autopilot in ACL2, Bill Young, July, 1996.
This paper presents an ACL2 translation of Butler's PVS formalization of a
simple autopilot.