Abstract:

The ACL2 theorem prover is an automatic theorem prover for Common Lisp,
developed by Matt Kaufmann and the author.  It is the most recent of a series
of Boyer-Moore provers starting with the Edinburgh Pure Lisp Theorem Prover
in the early 1970s.  ACL2 has seen sustained industrial use since the mid
1990s by companies including AMD, Centaur Technology, IBM, Intel, Kestrel
Institute, Motorola/Freescale, Oracle, and Rockwell Collins.  Among the
strengths of ACL2 that make it well-suited for certain industrial
applications is that it supports an ANSI standard programming language as its
logic, models built with ACL2 are efficiently executed (so they can be used
as prototypes and simulation engines), and the prover can be configured to be
fully automatic.  This talk presents ACL2 through a graduated series of
examples that illustrate the evolving strengths of the Boyer-Moore provers
over their 45 year history and the requirements of industrial applications.