### 395T Topics in Theorem Proving: ACL2

## Schedule Details

Fall, 2000

- Instructor: J Strother Moore
- Unique Id: 51510
- Meets: TT 11:00 am - 12:30 pm TAY 3.144
- Office Hours: TT 12:30-1:30 pm (or by appointment as needed)

## Syllabus

``ACL2'' stands for ``A Computational Logic for Applicative Common Lisp.''
It is a functional programming language, a mathematical logic and a
mechanical theorem prover for that logic. ACL2 is used to model computing
systems -- both hardware and software -- and to prove properties of those
models. The ACL2 home page is
http://www.cs.utexas.edu/users/moore/acl2. ACL2 is used primarily in
industry to prove properties of microprocessors. For example, the IEEE
compliance of the RTL implementing the elementary floating-point operations
on the AMD Athlon (TM) microprocessor was proved by David Russinoff using
ACL2, and ACL2 was used at Rockwell-Collins to model the JEM1 microprocessor,
the world's first silicon Java Virtual Machine. These and many other
applications are described in http://www.cs.utexas.edu/users/moore/publications/acl2-papers.html.

In this class you will learn how to use ACL2. The class will start
with an introduction to Lisp and to ACL2. You will then be given
elementary exercises to do with ACL2 and we will gradually build up to
more elaborate examples such as the modelling of simple programming
languages, compilers, and architectures.

You will be expected to use ACL2 to do the assignments. ACL2 is
freely available on the net (see the ACL2 home page).
ACL2 can be installed on top of any Common Lisp. ACL2 is installed
under the departmental Unix/Linux machines under /p/bin/acl2.
Extensive hypertext documentation
is available.

As a side-effect of the course, I hope to develop a FAQ for ACL2 for
new users.

PhD dissertation topics in this area include new theorem proving
techniques, new and effective models of computational systems
(especially parallel and distributed systems), effective embeddings or
connections to other formal systems such as model checking, Unity and
TLA, proof management tools, and interface and visualization tools.

## Prerequisites

The ideal prerequisite is to have taken CS389R (Recursion and
Induction). Alternatively, knowledge of Common Lisp and familiarity
with mathematical logic is very helpful. However, the course is open
to any graduate student.

## Textbooks

*Computer-Aided Reasoning: An Approach*, Kaufmann, Manolios, and Moore,
Kluwer, 2000.

## Tests and Grades

Grades will be based on class
participation.